1 (* Copyright (C) 2004-2005, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://helm.cs.unibo.it/
30 let debug_print = if debug then prerr_endline else ignore
32 (** raised when one of the script margins (top or bottom) is reached *)
35 let safe_substring s i j =
36 try String.sub s i j with Invalid_argument _ -> assert false
38 let heading_nl_RE = Pcre.regexp "^\\s*\n\\s*"
39 let heading_nl_RE' = Pcre.regexp "^(\\s*\n\\s*)((.|\n)*)"
40 let only_dust_RE = Pcre.regexp "^(\\s|\n|%%[^\n]*\n)*$"
41 let multiline_RE = Pcre.regexp "^\n[^\n]+$"
42 let newline_RE = Pcre.regexp "\n"
45 if Pcre.pmatch ~rex:multiline_RE str then
46 "\n(** " ^ (Pcre.replace ~rex:newline_RE str) ^ " *)"
48 "\n(**\n" ^ str ^ "\n*)"
51 let s = Pcre.replace ~rex:heading_nl_RE s in
53 let nl_pos = String.index s '\n' in
57 (** creates a statement AST for the Goal tactic, e.g. "goal 7" *)
59 let module A = GrafiteAst in
60 let loc = DisambiguateTypes.dummy_floc in
61 A.Executable (loc, A.Tactical (loc, A.Tactic (loc, A.Goal (loc, n))))
64 mathviewer:MatitaTypes.mathViewer;
65 urichooser: UriManager.uri list -> UriManager.uri list;
66 ask_confirmation: title:string -> message:string -> [`YES | `NO | `CANCEL];
67 develcreator: containing:string option -> unit;
68 mutable filenamedata: string option * MatitamakeLib.development option
71 let eval_with_engine guistuff status user_goal parsed_text st =
72 let module TA = GrafiteAst in
73 let module TAPp = GrafiteAstPp in
75 match guistuff.filenamedata with
77 | None,Some devel -> [MatitamakeLib.root_for_development devel ]
79 match MatitamakeLib.development_for_dir (Filename.dirname f) with
81 | Some devel -> [MatitamakeLib.root_for_development devel ]
83 let parsed_text_length = String.length parsed_text in
85 match st with TA.Executable (loc,ex) -> loc, ex | _ -> assert false in
86 let initial_space,parsed_text =
88 let pieces = Pcre.extract ~rex:heading_nl_RE' parsed_text in
89 pieces.(1), pieces.(2)
91 Not_found -> "", parsed_text in
92 (* we add the goal command if needed *)
93 let inital_space,new_status,new_status_and_text_list' =
94 match status.proof_status with
95 | Incomplete_proof (_, goal) when goal <> user_goal ->
97 MatitaEngine.eval_ast ~include_paths:include_
98 ~do_heavy_checks:true status (goal_ast user_goal) in
100 if initial_space = "" then "\n" else initial_space
103 [status, initial_space ^ TAPp.pp_tactic (TA.Goal (loc, user_goal))]
104 | _ -> initial_space,status,[] in
106 MatitaEngine.eval_ast
107 ~include_paths:include_ ~do_heavy_checks:true new_status st
111 | TA.Command (_, TA.Alias _)
112 | TA.Command (_, TA.Include _)
113 | TA.Command (_, TA.Interpretation _) ->
114 DisambiguateTypes.Environment.empty
115 | _ -> MatitaSync.alias_diff ~from:status new_status
117 (* we remove the defined object since we consider them "automatic aliases" *)
118 let initial_space,status,new_status_and_text_list_rev =
119 let module DTE = DisambiguateTypes.Environment in
120 let module UM = UriManager in
122 fun k ((v,_) as value) (initial_space,status,acc) ->
125 let v = UM.strip_xpointer (UM.uri_of_string v) in
126 List.exists (fun (s,_) -> s = v) new_status.objects
127 with UM.IllFormedUri _ -> false
130 initial_space,status,acc
134 if initial_space = "" then "\n" else initial_space in
136 DisambiguatePp.pp_environment(DTE.add k value DTE.empty) in
138 MatitaSync.set_proof_aliases status (DTE.add k value status.aliases)
140 "\n",new_status,((new_status, new_text)::acc)
141 ) new_aliases (initial_space,status,[]) in
142 let parsed_text = initial_space ^ parsed_text in
144 List.rev new_status_and_text_list_rev @ new_status_and_text_list' @
145 [new_status, parsed_text]
147 res,parsed_text_length
149 let eval_with_engine guistuff status user_goal parsed_text st =
151 eval_with_engine guistuff status user_goal parsed_text st
153 | MatitaEngine.UnableToInclude what
154 | MatitaEngine.IncludedFileNotCompiled what as exc ->
155 let compile_needed_and_go_on d =
158 while Glib.Main.pending () do ignore(Glib.Main.iteration false); done
160 if not(MatitamakeLib.build_development_in_bg ~target refresh_cb d) then
163 eval_with_engine guistuff status user_goal parsed_text st
165 let do_nothing () = [], 0 in
166 let handle_with_devel d =
167 let name = MatitamakeLib.name_for_development d in
168 let title = "Unable to include " ^ what in
170 what ^ " is handled by development <b>" ^ name ^ "</b>.\n\n" ^
171 "<i>Should I compile it and Its dependencies?</i>"
173 (match guistuff.ask_confirmation ~title ~message with
174 | `YES -> compile_needed_and_go_on d
176 | `CANCEL -> do_nothing ())
178 let handle_without_devel filename =
179 let title = "Unable to include " ^ what in
181 what ^ " is <b>not</b> handled by a development.\n" ^
182 "All dependencies are authomatically solved for a development.\n\n" ^
183 "<i>Do you want to set up a development?</i>"
185 (match guistuff.ask_confirmation ~title ~message with
189 guistuff.develcreator ~containing:(Some (Filename.dirname f))
190 | None -> guistuff.develcreator ~containing:None);
193 | `CANCEL -> do_nothing())
195 match guistuff.filenamedata with
196 | None,None -> handle_without_devel None
197 | None,Some d -> handle_with_devel d
199 match MatitamakeLib.development_for_dir (Filename.dirname f) with
200 | None -> handle_without_devel (Some f)
201 | Some d -> handle_with_devel d
204 let disambiguate term status =
205 let module MD = MatitaDisambiguator in
206 let dbd = MatitaDb.instance () in
207 let metasenv = MatitaMisc.get_proof_metasenv status in
208 let context = MatitaMisc.get_proof_context status in
210 MD.disambiguate_term ~dbd ~context ~metasenv ~aliases:status.aliases
211 ~universe:(Some status.multi_aliases) term in
216 let eval_macro guistuff status unparsed_text parsed_text script mac =
217 let module TA = GrafiteAst in
218 let module TAPp = GrafiteAstPp in
219 let module MQ = MetadataQuery in
220 let module MDB = MatitaDb in
221 let module CTC = CicTypeChecker in
222 let module CU = CicUniv in
223 (* no idea why ocaml wants this *)
224 let advance ?statement () = script#advance ?statement () in
225 let parsed_text_length = String.length parsed_text in
226 let dbd = MatitaDb.instance () in
229 | TA.WMatch (loc, term) ->
230 let term = disambiguate term status in
231 let l = MQ.match_term ~dbd term in
233 MatitaMisc.strip_suffix ~suffix:"."
234 (MatitaMisc.trim_blanks unparsed_text)
236 let entry = `Whelp (query_url, l) in
237 guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
238 [], parsed_text_length
239 | TA.WInstance (loc, term) ->
240 let term = disambiguate term status in
241 let l = MQ.instance ~dbd term in
242 let entry = `Whelp (TAPp.pp_macro_cic (TA.WInstance (loc, term)), l) in
243 guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
244 [], parsed_text_length
245 | TA.WLocate (loc, s) ->
246 let l = MQ.locate ~dbd s in
247 let entry = `Whelp (TAPp.pp_macro_cic (TA.WLocate (loc, s)), l) in
248 guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
249 [], parsed_text_length
250 | TA.WElim (loc, term) ->
251 let term = disambiguate term status in
254 | Cic.MutInd (uri,n,_) -> UriManager.uri_of_uriref uri n None
255 | _ -> failwith "Not a MutInd"
257 let l = MQ.elim ~dbd uri in
258 let entry = `Whelp (TAPp.pp_macro_cic (TA.WElim (loc, term)), l) in
259 guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
260 [], parsed_text_length
261 | TA.WHint (loc, term) ->
262 let term = disambiguate term status in
263 let s = ((None,[0,[],term], Cic.Meta (0,[]) ,term),0) in
264 let l = List.map fst (MQ.experimental_hint ~dbd s) in
265 let entry = `Whelp (TAPp.pp_macro_cic (TA.WHint (loc, term)), l) in
266 guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
267 [], parsed_text_length
270 let s = MatitaMisc.get_proof_status status in
271 let l = List.map fst (MQ.experimental_hint ~dbd s) in
272 let selected = guistuff.urichooser l in
274 | [] -> [], parsed_text_length
280 TA.Apply (loc, CicNotationPt.Uri (UriManager.string_of_uri uri,None))))))
282 let new_status = MatitaEngine.eval_ast status ast in
284 comment parsed_text ^
285 "\n" ^ TAPp.pp_statement ast
287 [ new_status , extra_text ], parsed_text_length
290 "The result of the urichooser should be only 1 uri, not:\n";
292 fun u -> MatitaLog.error (UriManager.string_of_uri u ^ "\n")
295 | TA.Check (_,term) ->
296 let metasenv = MatitaMisc.get_proof_metasenv status in
297 let context = MatitaMisc.get_proof_context status in
299 MatitaDisambiguator.disambiguate_term ~dbd ~context ~metasenv
300 ~aliases:status.aliases ~universe:(Some status.multi_aliases) term
302 let _, metasenv , term, ugraph =
307 let ty,_ = CTC.type_of_aux' metasenv context term ugraph in
308 let t_and_ty = Cic.Cast (term,ty) in
309 guistuff.mathviewer#show_entry (`Cic (t_and_ty,metasenv));
310 [], parsed_text_length
313 let status = script#status.proof_status in
316 | _ -> script#retract ();go_back()
318 [], parsed_text_length, Some go_back
319 | TA.Redo (_, Some i) -> [], parsed_text_length,
320 Some (fun () -> for j = 1 to i do advance () done)
321 | TA.Redo (_, None) -> [], parsed_text_length,
322 Some (fun () -> advance ())
323 | TA.Undo (_, Some i) -> [], parsed_text_length,
324 Some (fun () -> for j = 1 to i do script#retract () done)
325 | TA.Undo (_, None) -> [], parsed_text_length,
326 Some (fun () -> script#retract ()) *)
328 | TA.Quit _ -> failwith "not implemented"
329 | TA.Print (_,kind) -> failwith "not implemented"
330 | TA.Search_pat (_, search_kind, str) -> failwith "not implemented"
331 | TA.Search_term (_, search_kind, term) -> failwith "not implemented"
334 let eval_executable guistuff status user_goal unparsed_text parsed_text script
337 let module TA = GrafiteAst in
338 let module TAPp = GrafiteAstPp in
339 let module MD = MatitaDisambiguator in
340 let module ML = MatitacleanLib in
341 let parsed_text_length = String.length parsed_text in
343 | TA.Command (loc, _) | TA.Tactical (loc, _) ->
345 (match MatitaMisc.baseuri_of_baseuri_decl (TA.Executable (loc,ex)) with
348 if not (MatitaMisc.is_empty u) then
350 guistuff.ask_confirmation
351 ~title:"Baseuri redefinition"
353 "Baseuri " ^ u ^ " already exists.\n" ^
354 "Do you want to redefine the corresponding "^
355 "part of the library?")
357 | `YES -> MatitacleanLib.clean_baseuris [u]
359 | `CANCEL -> raise MatitaTypes.Cancel);
361 guistuff status user_goal parsed_text (TA.Executable (loc, ex))
362 with MatitaTypes.Cancel -> [], 0)
363 | TA.Macro (_,mac) ->
364 eval_macro guistuff status unparsed_text parsed_text script mac
366 let rec eval_statement baseoffset parsedlen error_tag (buffer : GText.buffer)
367 guistuff status user_goal script unparsed_text
369 if Pcre.pmatch ~rex:only_dust_RE unparsed_text then raise Margin;
372 GrafiteParser.parse_statement (Stream.of_string unparsed_text)
374 CicNotationParser.Parse_error (floc,err) as exc ->
375 let (x, y) = CicNotationPt.loc_of_floc floc in
376 let x = parsedlen + x in
377 let y = parsedlen + y in
378 let x' = baseoffset + x in
379 let y' = baseoffset + y in
380 let x_iter = buffer#get_iter (`OFFSET x') in
381 let y_iter = buffer#get_iter (`OFFSET y') in
382 buffer#apply_tag error_tag ~start:x_iter ~stop:y_iter;
386 (buffer#connect#changed
389 buffer#remove_tag error_tag ~start:buffer#start_iter
390 ~stop:buffer#end_iter;
392 None -> assert false (* a race condition occurred *)
394 (new GObj.gobject_ops buffer#as_buffer)#disconnect id));
395 let flocb,floce = floc in
397 {flocb with Lexing.pos_cnum = x}, {floce with Lexing.pos_cnum = y } in
398 raise (CicNotationParser.Parse_error (floc,err))
400 let text_of_loc loc =
401 let parsed_text_length = snd (CicNotationPt.loc_of_floc loc) in
402 let parsed_text = safe_substring unparsed_text 0 parsed_text_length in
403 parsed_text, parsed_text_length
406 | GrafiteAst.Comment (loc, _) ->
407 let parsed_text, parsed_text_length = text_of_loc loc in
408 let remain_len = String.length unparsed_text - parsed_text_length in
409 let s = String.sub unparsed_text parsed_text_length remain_len in
411 eval_statement baseoffset (parsedlen + parsed_text_length) error_tag
412 buffer guistuff status user_goal script s
415 | (status, text) :: tl ->
416 ((status, parsed_text ^ text)::tl), (parsed_text_length + len)
418 | GrafiteAst.Executable (loc, ex) ->
419 let parsed_text, parsed_text_length = text_of_loc loc in
420 eval_executable guistuff status user_goal unparsed_text parsed_text
423 let fresh_script_id =
427 class script ~(source_view: GSourceView.source_view)
428 ~(init: MatitaTypes.status)
429 ~(mathviewer: MatitaTypes.mathViewer)
435 let buffer = source_view#buffer in
436 let source_buffer = source_view#source_buffer in
438 val scriptId = fresh_script_id ()
441 mathviewer = mathviewer;
442 urichooser = urichooser;
443 ask_confirmation = ask_confirmation;
444 develcreator = develcreator;
445 filenamedata = (None, None)}
447 method private getFilename =
448 match guistuff.filenamedata with Some f,_ -> f | _ -> assert false
450 method private ppFilename =
451 match guistuff.filenamedata with
453 | None,_ -> sprintf ".unnamed%d.ma" scriptId
456 ignore (GMain.Timeout.add ~ms:300000
457 ~callback:(fun _ -> self#_saveToBackupFile ();true));
458 ignore (buffer#connect#modified_changed
459 (fun _ -> set_star (Filename.basename self#ppFilename) buffer#modified))
461 val mutable statements = []; (** executed statements *)
462 val mutable history = [ init ];
463 (** list of states before having executed statements. Head element of this
464 * list is the current state, last element is the state at the beginning of
466 * Invariant: this list length is 1 + length of statements *)
468 (** goal as seen by the user (i.e. metano corresponding to current tab) *)
469 val mutable userGoal = ~-1
471 (** text mark and tag representing locked part of a script *)
473 buffer#create_mark ~name:"locked" ~left_gravity:true buffer#start_iter
474 val locked_tag = buffer#create_tag [`BACKGROUND "lightblue"; `EDITABLE false]
475 val error_tag = buffer#create_tag [`UNDERLINE `SINGLE; `FOREGROUND "red"]
477 method locked_mark = locked_mark
478 method locked_tag = locked_tag
480 (* history can't be empty, the invariant above grant that it contains at
481 * least the init status *)
482 method status = match history with hd :: _ -> hd | _ -> assert false
484 method private _advance ?statement () =
485 let s = match statement with Some s -> s | None -> self#getFuture in
486 MatitaLog.debug ("evaluating: " ^ first_line s ^ " ...");
487 let (entries, parsed_len) =
488 eval_statement (buffer#get_iter_at_mark (`MARK locked_mark))#offset 0
489 error_tag buffer guistuff self#status userGoal self s
491 let (new_statuses, new_statements) = List.split entries in
492 history <- List.rev new_statuses @ history;
493 statements <- List.rev new_statements @ statements;
494 let start = buffer#get_iter_at_mark (`MARK locked_mark) in
495 let new_text = String.concat "" new_statements in
496 if statement <> None then
497 buffer#insert ~iter:start new_text
499 if new_text <> String.sub s 0 parsed_len then
501 let stop = start#copy#forward_chars parsed_len in
502 buffer#delete ~start ~stop;
503 buffer#insert ~iter:start new_text;
505 self#moveMark (String.length new_text)
507 method private _retract offset status new_statements new_history =
508 let cur_status = match history with s::_ -> s | [] -> assert false in
509 MatitaSync.time_travel ~present:cur_status ~past:status;
510 statements <- new_statements;
511 history <- new_history;
512 self#moveMark (- offset)
514 method advance ?statement () =
516 self#_advance ?statement ();
519 | Margin -> self#notify
520 | exc -> self#notify; raise exc
524 let cmp,new_statements,new_history,status =
525 match statements,history with
526 stat::statements, _::(status::_ as history) ->
527 String.length stat, statements, history, status
528 | [],[_] -> raise Margin
529 | _,_ -> assert false
531 self#_retract cmp status new_statements new_history;
534 | Margin -> self#notify
535 | exc -> self#notify; raise exc
537 method private getFuture =
538 buffer#get_text ~start:(buffer#get_iter_at_mark (`MARK locked_mark))
539 ~stop:buffer#end_iter ()
542 (** @param rel_offset relative offset from current position of locked_mark *)
543 method private moveMark rel_offset =
544 let mark = `MARK locked_mark in
545 let old_insert = buffer#get_iter_at_mark `INSERT in
546 buffer#remove_tag locked_tag ~start:buffer#start_iter ~stop:buffer#end_iter;
547 let current_mark_pos = buffer#get_iter_at_mark mark in
549 match rel_offset with
550 | 0 -> current_mark_pos
551 | n when n > 0 -> current_mark_pos#forward_chars n
552 | n (* when n < 0 *) -> current_mark_pos#backward_chars (abs n)
554 buffer#move_mark mark ~where:new_mark_pos;
555 buffer#apply_tag locked_tag ~start:buffer#start_iter ~stop:new_mark_pos;
556 buffer#move_mark `INSERT old_insert;
558 match self#status.proof_status with
559 Incomplete_proof (_,goal) -> self#setGoal goal
562 let mark_position = buffer#get_iter_at_mark mark in
563 if source_view#move_mark_onscreen mark then
565 buffer#move_mark mark mark_position;
566 source_view#scroll_to_mark ~use_align:true ~xalign:1.0 ~yalign:0.1 mark;
568 while Glib.Main.pending () do ignore(Glib.Main.iteration false); done
570 method clean_dirty_lock =
571 let lock_mark_iter = buffer#get_iter_at_mark (`MARK locked_mark) in
572 buffer#remove_tag locked_tag ~start:buffer#start_iter ~stop:buffer#end_iter;
573 buffer#apply_tag locked_tag ~start:buffer#start_iter ~stop:lock_mark_iter
575 val mutable observers = []
577 method addObserver (o: MatitaTypes.status -> unit) =
578 observers <- o :: observers
580 method private notify =
581 let status = self#status in
582 List.iter (fun o -> o status) observers
584 method loadFromFile f =
585 buffer#set_text (MatitaMisc.input_file f);
587 buffer#set_modified false
589 method assignFileName file =
590 let abspath = MatitaMisc.absolute_path file in
591 let devel = MatitamakeLib.development_for_dir (Filename.dirname abspath) in
592 guistuff.filenamedata <- Some abspath, devel
594 method saveToFile () =
595 let oc = open_out self#getFilename in
596 output_string oc (buffer#get_text ~start:buffer#start_iter
597 ~stop:buffer#end_iter ());
599 buffer#set_modified false
601 method private _saveToBackupFile () =
602 if buffer#modified then
604 let f = self#ppFilename ^ "~" in
605 let oc = open_out f in
606 output_string oc (buffer#get_text ~start:buffer#start_iter
607 ~stop:buffer#end_iter ());
609 MatitaLog.debug ("backup " ^ f ^ " saved")
612 method private goto_top =
613 MatitaSync.time_travel ~present:self#status ~past:init
615 method private reset_buffer =
620 buffer#remove_tag locked_tag ~start:buffer#start_iter ~stop:buffer#end_iter;
621 buffer#move_mark (`MARK locked_mark) ~where:buffer#start_iter
625 source_buffer#begin_not_undoable_action ();
626 buffer#delete ~start:buffer#start_iter ~stop:buffer#end_iter;
627 source_buffer#end_not_undoable_action ();
628 buffer#set_modified false
631 let template = MatitaMisc.input_file BuildTimeConf.script_template in
632 buffer#insert ~iter:(buffer#get_iter `START) template;
633 guistuff.filenamedata <-
634 (None,MatitamakeLib.development_for_dir (Unix.getcwd ()));
635 buffer#set_modified false;
636 set_star (Filename.basename self#ppFilename) false
638 method goto (pos: [`Top | `Bottom | `Cursor]) () =
639 let old_locked_mark =
641 (buffer#create_mark ~name:"old_locked_mark"
642 ~left_gravity:true (buffer#get_iter_at_mark (`MARK locked_mark))) in
643 let getpos _ = buffer#get_iter_at_mark (`MARK locked_mark) in
644 let getoldpos _ = buffer#get_iter_at_mark old_locked_mark in
645 let dispose_old_locked_mark () = buffer#delete_mark old_locked_mark in
648 dispose_old_locked_mark ();
656 let newpos = getpos () in
657 if (getoldpos ())#compare newpos < 0 then
659 buffer#move_mark old_locked_mark newpos;
664 dispose_old_locked_mark ();
667 | Margin -> dispose_old_locked_mark (); self#notify
668 | exc -> dispose_old_locked_mark (); self#notify; raise exc)
670 let locked_iter () = buffer#get_iter_at_mark (`NAME "locked") in
671 let cursor_iter () = buffer#get_iter_at_mark `INSERT in
674 (buffer#create_mark ~name:"initial_insert"
675 ~left_gravity:true (cursor_iter ())) in
676 let dispose_remember () = buffer#delete_mark remember in
677 let remember_iter () =
678 buffer#get_iter_at_mark (`NAME "initial_insert") in
679 let cmp () = (locked_iter ())#offset - (remember_iter ())#offset in
681 let forward_until_cursor () = (* go forward until locked > cursor *)
684 if cmp () < 0 && (getoldpos ())#compare (getpos ()) < 0
687 buffer#move_mark old_locked_mark (getpos ());
693 let rec back_until_cursor len = (* go backward until locked < cursor *)
695 statements, (status::_ as history) when len <= 0 ->
696 self#_retract (icmp - len) status statements history
697 | statement::tl1, _::tl2 ->
698 back_until_cursor (len - String.length statement) (tl1,tl2)
699 | _,_ -> assert false
703 if icmp < 0 then (* locked < cursor *)
704 (forward_until_cursor (); self#notify)
705 else if icmp > 0 then (* locked > cursor *)
706 (back_until_cursor icmp (statements,history); self#notify)
707 else (* cursor = locked *)
711 dispose_old_locked_mark ();
713 | Margin -> dispose_remember (); dispose_old_locked_mark (); self#notify
714 | exc -> dispose_remember (); dispose_old_locked_mark ();
715 self#notify; raise exc)
717 method onGoingProof () =
718 match self#status.proof_status with
719 | No_proof | Proof _ -> false
720 | Incomplete_proof _ -> true
721 | Intermediate _ -> assert false
723 method proofStatus = MatitaMisc.get_proof_status self#status
724 method proofMetasenv = MatitaMisc.get_proof_metasenv self#status
725 method proofContext = MatitaMisc.get_proof_context self#status
726 method proofConclusion = MatitaMisc.get_proof_conclusion self#status
727 method setGoal n = userGoal <- n
730 let s = self#getFuture in
731 let rec is_there_and_executable s =
732 if Pcre.pmatch ~rex:only_dust_RE s then raise Margin;
733 let st = GrafiteParser.parse_statement (Stream.of_string s) in
735 | GrafiteAst.Comment (loc,_)->
736 let parsed_text_length = snd (CicNotationPt.loc_of_floc loc) in
737 let remain_len = String.length s - parsed_text_length in
738 let next = String.sub s parsed_text_length remain_len in
739 is_there_and_executable next
740 | GrafiteAst.Executable (loc, ex) -> false
743 is_there_and_executable s
745 | CicNotationParser.Parse_error _ -> false
752 MatitaLog.debug "script status:";
753 MatitaLog.debug ("history size: " ^ string_of_int (List.length history));
754 MatitaLog.debug (sprintf "%d statements:" (List.length statements));
755 List.iter MatitaLog.debug statements;
756 MatitaLog.debug ("Current file name: " ^
757 (match guistuff.filenamedata with
758 |None,_ -> "[ no name ]"
763 let _script = ref None
765 let script ~source_view ~init ~mathviewer ~urichooser ~develcreator ~ask_confirmation ~set_star ()
768 ~source_view ~init ~mathviewer ~ask_confirmation ~urichooser ~develcreator ~set_star ()
773 let instance () = match !_script with None -> assert false | Some s -> s