Vous avez reçu un message "Your GitLab account has been locked ..." ? Pas d'inquiétude : lisez cet article https://docs.gricad-pages.univ-grenoble-alpes.fr/help/unlock/

xlurette_glade_main.ml 23.1 KB
Newer Older
1
2
3
open GMain
open GEdit

4
5
6
let debug = 
(*   true *)
  false
7

8
let pid = ref 0
9
let lpid = ref 0
10

11

12
13
14
(* Flag telling if any saved package need to be restored *)
let restore = ref false

15

16
17
18
let (lurette_stdin_in, lurette_stdin_out) = Unix.pipe ()
let (lurette_stdout_in, lurette_stdout_out) = Unix.pipe ()
 
19

20
21
let ic = Unix.in_channel_of_descr lurette_stdout_in
let oc = Unix.out_channel_of_descr lurette_stdin_out
22
23


24
25
26
27
let _ = 
  set_binary_mode_in ic  false;
  set_binary_mode_out oc false  
    (* XXX won't work under window$ !!! *)
28
(*   ; Unix.set_nonblock lurette_stdout_out *)
29
  ; Unix.set_nonblock lurette_stdout_in
30

31
type draw_mode = Vertices | Edges | Inside
32
type tok = Genlex.token Stream.t
33

34
35
let ok_str = "   OK!
"
36
37
(**************************************************************************)
(**************************************************************************)
38
39
class customized_callbacks = object(self)
  inherit Xlurette_glade_callbacks.default_callbacks
40
41
    

42
43
  method put str = self#top_xlurette#output_window#insert str

44
45
46
47
48
49
50
51
52
53
54
55
56
57
  method read_pipe () =
    let length = float_of_string self#top_xlurette#test_length#text in
    let 
      display = self#top_xlurette#output_window#insert
    and 
      progress = 
      ( fun f ->
	  let p = f /. length in 
	  let pi = int_of_float (p *. 100.) in
	    self#top_xlurette#step_number_label#set_text
	      ((string_of_int pi) ^ " %  \n(" ^ (string_of_int (int_of_float f))
	       ^ "/" ^ (string_of_int (int_of_float length)) ^ ")");
	    self#top_xlurette#progressbar#set_percentage p )
    in
58

59
60
61
62
63
64
      ( try    
	  while true do
	    let str = input_line ic in
	      if debug then (print_string  (str ^ "\n"); flush stdout);
	      
	      if 
65
66
67
68
		str = "" 
	      then 
		()
	      else if 
69
70
71
72
73
74
75
76
77
78
79
80
		str = "One more loop ? [type any char to stop, `CR' to continue]"
	      then
		display (
		  "One more loop ?
      click on the step (resp. stop) button to continue (resp. stop)\n")
	      else if 
		str = "  Type h for help, or man for a small user manual."
	      then
		(
		  display "No program is currently running.\n";
		  ()
		)
81
82
83
84
85
86
87
88
	      else if 
		String.length str > 22 
		&& String.sub str 0 22 = "The Pid of lurette is " 
	      then
		let lurette_pid = String.sub str 22 ((String.length str) - 22) in
		  lpid := int_of_string lurette_pid;
		  ()
	      
89
	      else if 
90
91
		String.length str > 36 
		&& String.sub str 0 34 = "The random engine was initialized " 
92
93
94
	      then
		let seed_str = String.sub str 48 ((String.length str) - 48) in
		  self#top_xlurette#user_seed#set_text seed_str;
95
96
97
98
99
100
		  if self#top_xlurette#radiobutton_verbose_on#active then
		    display (str ^ "\n");
	      else if 
		str = " ==> The test completed; no property has been violated."
	      then
		display (ok_str ^ str ^ "\n")
101
102
103
104
	      else if 
		String.length str > 7 && String.sub str 0 8 = "<lurette" 
	      then
		()
105
106
107
108
109
110
111
112
113
114
115
	      else if 
		((String.length str > 9) && ((String.sub str 0 9) = "--- step "))
	      then
		(
		  let dot_index = String.index str ':' in
		  let step_str = String.sub str 9 (dot_index-9) in
		  let stepf = float_of_string step_str in
		    progress stepf;
		    if self#top_xlurette#radiobutton_verbose_on#active then
		      display (str ^ "\n")
		)
116
	      else
117
118
119
		display (str ^ "\n")
	  done
	with _ -> () 
120
121
      );
      true
122
	
123
124
125

  method show_step_window () = 
    self#top_step_by_step_window#step_by_step_window#show ()
126
      
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158


  (* sut file selection window *)
  method browse_sut_clicked () = 
    self#top_fileselection_sut#fileselection_sut#show ()

  method ok_sut_clicked () = 
    let sut_file = self#top_fileselection_sut#fileselection_sut#get_filename in
      self#top_xlurette#sut_name#set_text sut_file ;
      self#top_fileselection_sut#fileselection_sut#misc#hide ()

  method cancel_sut_clicked () = 
    self#top_fileselection_sut#fileselection_sut#misc#hide ()


  (* oracle file selection window *)
  method browse_oracle_clicked () = 
    self#top_fileselection_oracle#fileselection_oracle#show ()

  method ok_oracle_clicked () = 
    let oracle_file = self#top_fileselection_oracle#fileselection_oracle#get_filename in
      self#top_xlurette#oracle_name#set_text oracle_file ;
      self#top_fileselection_oracle#fileselection_oracle#misc#hide ()

  method cancel_oracle_clicked () = 
    self#top_fileselection_oracle#fileselection_oracle#misc#hide ()


  (* env file selection window *)
  method browse_env_clicked () = 
    self#top_fileselection_env#fileselection_env#show ()

159
160
161
  method add_env_clicked () = 
    self#top_fileselection_add_env#fileselection_add_env#show ()

162
163
  method ok_env_clicked () = 
    let env_file = self#top_fileselection_env#fileselection_env#get_filename in
164
      self#top_xlurette#env_name#set_text  env_file ;
165
166
      self#top_fileselection_env#fileselection_env#misc#hide ()

167
168
169
170
171
172
  method ok_add_env_clicked () = 
    let env_file = self#top_fileselection_add_env#fileselection_add_env#get_filename in
      self#top_xlurette#env_name#set_text 
	(self#top_xlurette#env_name#text ^ " " ^ env_file) ;
      self#top_fileselection_add_env#fileselection_add_env#misc#hide ()

173
174
175
  method cancel_env_clicked () = 
    self#top_fileselection_env#fileselection_env#misc#hide ()

176
177
178
179
  method cancel_add_env_clicked () = 
    self#top_fileselection_add_env#fileselection_add_env#misc#hide ()


180
181
182
183
184
  method close_step_button_clicked () = 
    self#top_step_by_step_window#step_by_step_window#misc#hide ()


  method show_env_button_clicked () = 
185
186
187
188
189
190
    let env0 = self#top_xlurette#env_name#text in
    let env = 
      if Util.get_extension env0 = ".lut" 
      then ((Util.remove_extension env0) ^ ".luc")
      else env0
    in
191
192
193
194
    let cmd_show = ("set_env \"" ^ env ^ "\"\n show \n") in

      output_string oc cmd_show ;
      if debug then (output_string stderr cmd_show; flush stderr);
195
      flush oc
196

197
198

  method quit () = 
199
200
    output_string oc "quit\n";
    flush oc;
201
    prerr_endline "bye! " ; 
202
    Unix.kill !pid (Sys.sigkill);
203
    exit 0; ()
204
      
205
206
207
208
209
210
211
212
  method step () = 
    if 
      self#top_xlurette#radiobutton_step_yes#active
    then
      (
	let cmd_step = (" \n") in
	  if debug then (output_string stderr cmd_step; flush stderr);
	  output_string oc cmd_step;
213
	  flush oc
214
215
216
      )
    else
      self#top_xlurette#output_window#insert 
217
218
219
	"Step button unactive because step-by-step mode is off\n"

  method stop_run () = 
220
221
222
223
224
225
226
227
228
    if !lpid <> 0 then
      (
	self#top_xlurette#output_window#insert "Stopping the current run.\n";
	(try 
	   Unix.kill (!lpid) Sys.sigkill 
	 with _ -> ()
	);
	lpid := 0
      )
229
230
231
232
233
234
235
236
237

  method stop () = 
    if 
      self#top_xlurette#radiobutton_step_yes#active
    then
      (
	let cmd_stop = ("    \n") in
	  if debug then (output_string stderr cmd_stop; flush stderr);
	  output_string oc cmd_stop;
238
	  flush oc;    
239
	  self#top_step_by_step_window#step_by_step_window#misc#hide ()
240
241
242
243
      )
    else
      self#top_xlurette#output_window#insert 
	"Stop button unactive because step-by-step mode is off\n"      
244
	
245
246
247
248
249
250
251
252
253
  method display_rif_file_clicked () = 
    let cmd_display = 
      ("set_output " ^ self#top_xlurette#rif_file#text ^ "\n" ^
       "sim2chro\n") in
      output_string oc cmd_display ;
      if debug then output_string stderr cmd_display;

      flush oc;
      flush stderr
254

255
256
257
258
259
260
  method call_sim2chro_clicked () = 
    let cmd_display = 
      ("set_output " ^ self#top_xlurette#rif_file#text ^ "\n" ^
       "sim2chro\n") in
      output_string oc cmd_display ;
      if debug then output_string stderr cmd_display;
261

262
263
      flush oc;
      flush stderr
264

265
266

  method get_all_cmds () =
267
268
269
    let sut = self#top_xlurette#sut_name#text 
    and sut_node = self#top_xlurette#sut_node#text in
    let cmd_sut = ("set_sut \"" ^ sut ^ "\" \"" ^ sut_node ^ "\"\n") in
270

271
272
    let env = self#top_xlurette#env_name#text in
    let cmd_env = ("set_env \"" ^ env ^ "\"\n") in
273

274
275
    let oracle = self#top_xlurette#oracle_name#text 
    and oracle_node = self#top_xlurette#oracle_node#text  in
276
    let cmd_oracle = 
277
      ("set_oracle \"" ^ oracle ^ "\" \"" ^ oracle_node ^ "\"\n") in
278

279
    let test_length = self#top_xlurette#test_length#text in
280
281
    let cmd_test_length = ("set_test_length " ^ test_length ^ "\n") in

282
    let formula_nb = self#top_xlurette#formula_nb#text in
283
284
    let cmd_formula_nb = ("set_formula_nb " ^ formula_nb ^ "\n") in

285
    let draw_nb = self#top_xlurette#draw_nb#text in
286
287
    let cmd_draw_nb = ("set_draw_nb " ^ draw_nb ^ "\n") in

288
    let rif_file = self#top_xlurette#rif_file#text in
289
290
    let cmd_rif_file = ("set_output " ^ rif_file ^ "\n") in

291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
    let cmd_step =
      if self#top_xlurette#radiobutton_step_yes#active
      then "set_step_by_step true\n" 
      else "set_step_by_step false\n"
    in

    let cmd_seed =
      if self#top_xlurette#radiobutton_random_seed#active 
      then "set_seed_randomly \n" 
      else ("set_seed " ^ self#top_xlurette#user_seed#text ^ "\n")
    in

    let cmd_draw_mode =
      if self#top_xlurette#radiobutton_inside#active 
      then "set_draw_mode inside \n" 
      else if self#top_xlurette#radiobutton_edges#active 
      then "set_draw_mode edges \n" 
308
      else "set_draw_mode vertices \n" 
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
    in

    let cmd_call_sim2chro =
      if self#top_xlurette#radiobutton_call_sim2chro_yes#active 
      then "set_display_sim2chro true \n" 
      else "set_display_sim2chro false \n" 
    in

    let cmd_display_local =
      if self#top_xlurette#radiobutton_display_local_yes#active 
      then "set_display_local_var true \n" 
      else "set_display_local_var false \n" 
    in

    let cmd_verbose =
      if self#top_xlurette#radiobutton_verbose_on#active 
      then "set_verbose true \n" 
      else "set_verbose false \n" 
    in

329
330
331
332
333
    let cmd_show_step =
      if (self#top_xlurette#radiobutton_show_step_on#active 
	  || self#top_xlurette#radiobutton_verbose_on#active )
      then "set_show_step true \n" 
      else "set_show_step false \n" 
334
    in      
335
336
337
338
      cmd_oracle ^ cmd_test_length ^ cmd_formula_nb ^ cmd_draw_nb
      ^ cmd_rif_file ^ cmd_env ^ cmd_sut ^ cmd_step ^ cmd_seed
      ^ cmd_draw_mode ^ cmd_call_sim2chro ^ cmd_display_local
      ^ cmd_verbose ^ cmd_show_step 
339
	
340

341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
 method on_sut_name_changed () =
   if self#top_xlurette#sut_node#text = "" then
     let str = self#top_xlurette#sut_name#text in
     let base = Filename.basename str in
     let node = 
       try Filename.chop_extension base 
       with _ -> base
     in
       self#top_xlurette#sut_node#set_text node

 method on_oracle_name_changed () =
    if self#top_xlurette#oracle_node#text = "" then
      let str = self#top_xlurette#oracle_name#text in
      let base = Filename.basename str in
      let node = 
	try Filename.chop_extension base 
	with _ -> base
      in
	self#top_xlurette#oracle_node#set_text node

361
  method run_lurette () = 
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377

    if self#top_xlurette#env_name#text = "" 
    then 
      (
	let str = self#top_xlurette#sut_name#text in
     	let base = Filename.basename str in
	let node = 
	  try Filename.chop_extension base 
	  with _ -> base
	in
	  self#put "Since no environment is provided, I generate a fake one named\n";
	  self#put (node ^ "_env.lut, that you can edit and modify.\n\n");
	  Util.gen_fake_lutin (node ^ ".h") ;
	  self#top_xlurette#env_name#set_text (node ^ "_env.lut")
      );      

378
    let all_cmds = (self#get_all_cmds ()) ^ "run\n" in
379
380
381
      
      if self#top_xlurette#radiobutton_step_yes#active
      then self#top_step_by_step_window#step_by_step_window#show ();
382

383
384
      output_string oc all_cmds ;
      if debug then output_string stderr all_cmds;  
385
      flush oc;
386

387
      flush stderr
388

389
390
391
392
393
394
395
396
  method save_parameters () =
    let msg = "Saving current parameters in .lurette_rc \n"
    and cmds = self#get_all_cmds ()
    and file = open_out ".lurette_rc"
    in
      output_string file cmds;
      close_out file;
      self#top_xlurette#output_window#insert msg
397

398
399

  method save_session () =
400
    output_string oc ("pack " ^ self#top_xlurette#saved_session_file#text ^ " \n");
401
    flush oc;
402
403
    prerr_endline "save session ...";
    ()
404
405


406
407
408
409
  method get_env () =
    self#top_xlurette#env_name#text
  method set_env str =
    self#top_xlurette#env_name#set_text str
410

411
412
413
414
  method get_sut () =
    self#top_xlurette#sut_name#text
  method set_sut str =
    self#top_xlurette#sut_name#set_text str
415

416
417
418
419
420
  method get_sut_node () =
    self#top_xlurette#sut_node#text
  method set_sut_node str =
    self#top_xlurette#sut_node#set_text str

421
422
423
424
  method get_oracle () =
    self#top_xlurette#oracle_name#text
  method set_oracle str =
    self#top_xlurette#oracle_name#set_text str
425

426
427
428
429
430
431
  method get_oracle_node () =
    self#top_xlurette#oracle_node#text
  method set_oracle_node str =
    self#top_xlurette#oracle_node#set_text str


432
433
434
435
  method get_test_length () =
    int_of_string self#top_xlurette#test_length#text
  method set_test_length i =
    self#top_xlurette#test_length#set_text (string_of_int i)
436

437
438
439
440
441
  method get_seed () =
    int_of_string self#top_xlurette#user_seed#text
  method set_seed i =
    self#top_xlurette#user_seed#set_text (string_of_int i)

442
443
444
445
  method get_formula_nb () =
    int_of_string self#top_xlurette#formula_nb#text
  method set_formula_nb i =
    self#top_xlurette#formula_nb#set_text (string_of_int i)
446

447
448
449
450
  method get_draw_nb () =
    int_of_string self#top_xlurette#draw_nb#text
  method set_draw_nb i =
    self#top_xlurette#draw_nb#set_text (string_of_int i)
451

452
453
454
455
  method get_rif_file () =
    self#top_xlurette#rif_file#text
  method set_rif_file str =
    self#top_xlurette#rif_file#set_text str
456

457
458
459
460
  method get_restore () =
    self#top_xlurette#saved_session_file#text
  method set_restore str =
    self#top_xlurette#saved_session_file#set_text str
461

462
463
464
  method set_draw_mode dm =
    match dm with
	Edges -> self#top_xlurette#radiobutton_edges#set_active true
465
      | Vertices -> self#top_xlurette#radiobutton_vertices#set_active true
466
      | Inside -> self#top_xlurette#radiobutton_inside#set_active true
467

468
469
470
471
472


	  
  method read_commands line =
    let lexer = Genlex.make_lexer [] in
473
    
474
475
476
477
478
479
      
    let (parse_file_name : tok -> string) = 
      fun tok -> 
	try
	  match tok with parser 
	    | [<  'Genlex.String str >] -> 
480
		if str = "" then "" else Util.remove_extension str 
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
	    | [<  'Genlex.Ident id  >] -> id
	    | [<  >]  ->  "" 
	  with _ -> 
	    print_string 
	    "*** parse error: cannot parse that file name.\n";
	    flush stdout;
	    ""
    in
    let rec (parse_env : tok -> string) = 
      fun tok -> 
	try
	  (
	    match tok with parser 
	      | [<  'Genlex.Ident "x" ; tail = parse_env >] -> (" x " ^ tail)
	      | [<  'Genlex.String str ; tail = parse_env >] -> 
496
497
		  ( str ^ tail) 
	      | [<  'Genlex.Ident id  ; tail = parse_env >] -> (id ^ " " ^ tail)
498
499
500
501
502
503
504
505
506
507
	      | [< _ >]  ->  "" 
	  )
	with e -> 
	  print_string (Printexc.to_string e);
	  print_string 
            "*** Error when parsing the environment field.\n";
	  flush stdout;
	  ""
    in

508
    let rec read_cmd tok =
509
510
511
512
513
514
515
516
      (* : 'a -> tok -> unit) = *)
      
      ( match tok with parser
	  | [< 'Genlex.Ident "set_draw_mode" ;'Genlex.Ident id >] -> 
	      (
		match id with 
		    "inside" -> self#set_draw_mode Inside
		  | "edges"  -> self#set_draw_mode Edges
517
		  | "vertices" -> self#set_draw_mode Vertices
518
519
520
521
522
		  | _ -> print_string ("Unknown draw mode (" ^ id ^ ")\n")
	      )
	  | [< 'Genlex.Ident "set_env" ; 'Genlex.String str >] ->
	      self#set_env str
	      
523
524
525
	  | [< 'Genlex.Ident "set_sut" ; str = parse_file_name  ; node = parse_node>] -> 
	      self#set_sut str;
	      self#set_sut_node node
526
	      
527
528
529
	  | [< 'Genlex.Ident "set_oracle" ; str = parse_file_name  ; node = parse_node >] ->
	      self#set_oracle str;
	      self#set_oracle_node node
530
531
532
533
534
535
	      
	  | [< 'Genlex.Ident "set_test_length" ; 'Genlex.Int i >] ->
	      self#set_test_length i
	      
	  | [< 'Genlex.Ident "set_formula_nb" ; 'Genlex.Int i >] -> 
	      self#set_formula_nb i
536

537
538
539
540
	  | [< 'Genlex.Ident "set_draw_nb" ; 'Genlex.Int i >] -> 
	      self#set_draw_nb i
	      
	  | [< 'Genlex.Ident "set_seed" ; 'Genlex.Int i >] -> 
541
	      self#top_xlurette#radiobutton_user_seed#set_active true ;
542
	      self#set_seed i
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574

	  | [< 'Genlex.Ident "set_seed_randomly" >] -> 
	      self#top_xlurette#radiobutton_random_seed#set_active true 

	  | [< 'Genlex.Ident "set_step_by_step" ; 'Genlex.Ident id >] -> 
	      if id = "true" 
	      then self#top_xlurette#radiobutton_step_yes#set_active true 
	      else self#top_xlurette#radiobutton_step_no#set_active true 

	  | [< 'Genlex.Ident "set_display_sim2chro" ; 'Genlex.Ident id >] -> 
	      if id = "true" 
	      then self#top_xlurette#radiobutton_call_sim2chro_yes#set_active true 
	      else self#top_xlurette#radiobutton_call_sim2chro_no#set_active true 

	  | [< 'Genlex.Ident "set_display_local_var" ; 'Genlex.Ident id >] -> 
	      if id = "true" 
	      then self#top_xlurette#radiobutton_display_local_yes#set_active true 
	      else self#top_xlurette#radiobutton_display_local_no#set_active true 

	  | [< 'Genlex.Ident "set_verbose" ; 'Genlex.Ident id >] -> 
	      if id = "true" 
	      then self#top_xlurette#radiobutton_verbose_on#set_active true 
	      else self#top_xlurette#radiobutton_verbose_off#set_active true 

	  | [< 'Genlex.Ident "set_show_step" ; 'Genlex.Ident id >] -> 
	      if id = "true" 
	      then self#top_xlurette#radiobutton_show_step_on#set_active true 
	      else self#top_xlurette#radiobutton_show_step_off#set_active true 



	  | [< _ >] -> ()
575
      )    
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
and  
  (parse_node : tok -> string) = 
  fun tok -> 
    let str =
      try
	match tok with parser 
	  | [< 'Genlex.String id  >] -> id
	  | [< 'Genlex.Ident id  >] -> id
	  | [<   >] -> ""
	with _ -> 
	  ""
    in
    let base = Filename.basename str in
      try Filename.chop_extension base 
      with _ -> base
	
592
593
594
595
    in
      read_cmd (lexer (Stream.of_string line))


596
597
598
end


599
600
601
602
(**************************************************************************)
let usage = "
usage: xlurette [<options>] [<env ([x] env)*>]

603
604
xlurette is a Graphical interface over lurettetop, which lets
one automatically test reactive programs written in lustre.
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641

Command line <options> are:
"

let rec speclist callbacks = 
  [
    "--sut", Arg.String (fun s -> callbacks#set_sut s), 
       "<string>\tFile name of the system under test.";
    "-sut", Arg.String (fun s -> callbacks#set_sut s),
    " <string>\n" ;

    "--oracle", Arg.String (fun s -> callbacks#set_oracle s), 
       "<string>\tFile name of the oracle.";
    "-oracle", Arg.String (fun s -> callbacks#set_oracle s), " <string>\n";

    "--test-length", Arg.Int (fun i -> callbacks#set_test_length i),
       "<int>\tNumber of steps to be done";
    "-l", Arg.Int (fun i -> callbacks#set_test_length i),  
    ("<int>\t\t(default=" ^ (string_of_int (callbacks#get_test_length ())) ^ ").\n");

    "--thick-form", Arg.Int (fun i -> callbacks#set_formula_nb i),
       "<int>\tNumber of formula to be drawn at each step";
    "-tf", Arg.Int (fun i -> callbacks#set_formula_nb i), 
    ("<int>\t\t(default=" ^ (string_of_int (callbacks#get_formula_nb ())) ^ ").\n");

    "--thick-draw", Arg.Int (fun i -> callbacks#set_draw_nb i),
       "<int>\tNumber of draw to be done in each formula ";
    "-td", Arg.Int (fun i -> callbacks#set_draw_nb i),
    ("<int>\t\tat each step (default=" ^ 
     (string_of_int (callbacks#get_draw_nb ())) ^ ").\n");
    
    "--draw-inside", Arg.Unit (fun _ -> callbacks#set_draw_mode Inside),
       "\t\tDraw inside the polyhedron of solutions.\n ";

    "--draw-edges", Arg.Unit (fun _ -> callbacks#set_draw_mode Edges),
       "\t\tDraw on the edges of the polyhedron of solutions.\n ";

642
643
    "--draw-vertices", Arg.Unit (fun _ -> callbacks#set_draw_mode Vertices),
       "\t\tDraw among the vertices of the polyhedron of solutions.\n ";
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664



    "--output", Arg.String (fun s -> callbacks#set_rif_file s),
    ("<string>\tSet the output file name (default is \"" ^ 
    (callbacks#get_rif_file ()) ^ "\").");
    "-o", Arg.String (fun s -> callbacks#set_rif_file s), "<string>\n";


    "--restore", Arg.String (fun s -> callbacks#set_restore s; restore := true), 
       "<string>\tFile name (without extension) of the package containing"
       ^ "\n\t\t\tthe temporarily files to be restored (cf the pack command).\n";


    "--help", Arg.Unit (fun _ -> (Arg.usage (speclist callbacks) usage  ; exit 0)),
       "\t\tDisplay this list of options." ;
    "-help", Arg.Unit (fun _ -> (Arg.usage (speclist callbacks) usage  ; exit 0)),
    "";
    "-h", Arg.Unit (fun _ -> (Arg.usage (speclist callbacks) usage  ; exit 0)),
    ""
]
665
    
666

667
668
669
(******************************************************************************)


670

671
let main () = 
672
673
  let _ =
    let _ = 
674
      (* Check that LURETTE_PATH env var is set. *)
675
676
677
678
679
680
681
682
683
684
685
      try 
	Sys.getenv "LURETTE_PATH"
      with Not_found -> 
	(
	  print_string "*** Can not run xlurette, sorry. \n***";
	  print_string "You need to set the LURETTE_PATH env variable properly.\n";
	  flush stdout;
	  exit 2;
	) 
    in
      if not (Sys.file_exists "pixmaps")
686
687
	(* To turn around a bug in mlglade which searches the pixmaps dir
	   in the current dir instead of the xlurette one...  *)
688
689
      then
	try
690
	  (* XXX Won't work under window$ !!! *)
691
692
693
694
695
696
	  Unix.symlink 
	    (Filename.concat (Unix.getenv "LURETTE_PATH") "ihm/xlurette/pixmaps")
	    "pixmaps";
	with _ -> 
	  print_string "*** Can not create a file in the current directory.\n";
	  flush stdout
697
  in
698
699
  let callbacks = new customized_callbacks in
  let xlurette = new Xlurette_glade_interface.top_xlurette callbacks in
700
    
701
702
703
704
705
706
707
708
709
710
711
712
  let step_by_step = 
    new Xlurette_glade_interface.top_step_by_step_window callbacks 
  in
  let browse_sut = 
    new Xlurette_glade_interface.top_fileselection_sut callbacks 
  in
  let browse_oracle = 
    new Xlurette_glade_interface.top_fileselection_oracle callbacks 
  in
  let browse_env = 
    new Xlurette_glade_interface.top_fileselection_env callbacks 
  in
713
714
715
  let browse_add_env = 
    new Xlurette_glade_interface.top_fileselection_add_env callbacks 
  in
716
    (* msg generated by mlglade :
717
718
       You should probably remove the next line if you want to use the 
       event masks from glade 
719
    *)
720
  let _ = GtkBase.Widget.add_events xlurette#xlurette#as_widget [`ALL_EVENTS] in
721
  let args = 
722
    if !restore 
723
    then (* XXX Does not work. why ??? *)
724
725
726
727
      Array.of_list ["lurettetop"; "--restore"; (callbacks#get_restore ())]
    else
      Array.of_list ["lurettetop"]
  in
728
729
730
    pid := Unix.create_process "lurettetop" args
      lurette_stdin_in lurette_stdout_out Unix.stderr ;
    
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
    
    (* read command in the .lurette_rc file *)
    let lurette_rc =  ".lurette_rc" in

      (* read command in the .lurette_rc file *)
      ( 
	if Sys.file_exists lurette_rc then
	  let ic = (open_in lurette_rc) in
	  try
	    while true do
	      let _ = 
		callbacks#read_commands (input_line ic)
	      in
		()
	    done 
	  with End_of_file -> 
	    close_in ic 
      );
      
750

751
752
753
754
    (* 
       read the lurettetop command line options (that will override the 
       .lurette.=_rc ones) 
    *)
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
      let env_saved = callbacks#get_env () in
	callbacks#set_env "";
	( try 
	    Arg.parse (speclist callbacks)
		(fun s -> 
		   if s = "x" 
		   then callbacks#set_env ((callbacks#get_env ()) ^ " x ")
		   else callbacks#set_env ((callbacks#get_env ()) ^ " " ^ s )
		)
		usage
	  with 
	      Failure(e) ->
		(
		  print_string e;
		  flush stdout ;
		  flush stderr ;
		  exit 2
		)
	    | _ ->
774
	      exit 2 
775
776
	);
	if (callbacks#get_env () = "") then callbacks#set_env env_saved;
777

778
779
780
	xlurette#xlurette#show() ;
	
	let _ = Timeout.add ~ms:100 ~callback:callbacks#read_pipe in
781
	
782
	  Main.main ()
783
784
785



786
787
788

let _ = Printexc.print main ()