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.cons k value DTE.empty) in
138 {status with aliases = DTE.cons 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
209 let aliases = MatitaMisc.get_proof_aliases status in
210 let interps = MD.disambiguate_term dbd context metasenv aliases term in
215 let eval_macro guistuff status unparsed_text parsed_text script mac =
216 let module TA = GrafiteAst in
217 let module TAPp = GrafiteAstPp in
218 let module MQ = MetadataQuery in
219 let module MDB = MatitaDb in
220 let module CTC = CicTypeChecker in
221 let module CU = CicUniv in
222 (* no idea why ocaml wants this *)
223 let advance ?statement () = script#advance ?statement () in
224 let parsed_text_length = String.length parsed_text in
225 let dbd = MatitaDb.instance () in
228 | TA.WMatch (loc, term) ->
229 let term = disambiguate term status in
230 let l = MQ.match_term ~dbd term in
232 MatitaMisc.strip_suffix ~suffix:"."
233 (MatitaMisc.trim_blanks unparsed_text)
235 let entry = `Whelp (query_url, l) in
236 guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
237 [], parsed_text_length
238 | TA.WInstance (loc, term) ->
239 let term = disambiguate term status in
240 let l = MQ.instance ~dbd term in
241 let entry = `Whelp (TAPp.pp_macro_cic (TA.WInstance (loc, term)), l) in
242 guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
243 [], parsed_text_length
244 | TA.WLocate (loc, s) ->
245 let l = MQ.locate ~dbd s in
246 let entry = `Whelp (TAPp.pp_macro_cic (TA.WLocate (loc, s)), l) in
247 guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
248 [], parsed_text_length
249 | TA.WElim (loc, term) ->
250 let term = disambiguate term status in
253 | Cic.MutInd (uri,n,_) -> UriManager.uri_of_uriref uri n None
254 | _ -> failwith "Not a MutInd"
256 let l = MQ.elim ~dbd uri in
257 let entry = `Whelp (TAPp.pp_macro_cic (TA.WElim (loc, term)), l) in
258 guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
259 [], parsed_text_length
260 | TA.WHint (loc, term) ->
261 let term = disambiguate term status in
262 let s = ((None,[0,[],term], Cic.Meta (0,[]) ,term),0) in
263 let l = List.map fst (MQ.experimental_hint ~dbd s) in
264 let entry = `Whelp (TAPp.pp_macro_cic (TA.WHint (loc, term)), l) in
265 guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
266 [], parsed_text_length
269 let s = MatitaMisc.get_proof_status status in
270 let l = List.map fst (MQ.experimental_hint ~dbd s) in
271 let selected = guistuff.urichooser l in
273 | [] -> [], parsed_text_length
279 TA.Apply (loc, CicNotationPt.Uri (UriManager.string_of_uri uri,None))))))
281 let new_status = MatitaEngine.eval_ast status ast in
283 comment parsed_text ^
284 "\n" ^ TAPp.pp_statement ast
286 [ new_status , extra_text ], parsed_text_length
289 "The result of the urichooser should be only 1 uri, not:\n";
291 fun u -> MatitaLog.error (UriManager.string_of_uri u ^ "\n")
294 | TA.Check (_,term) ->
295 let metasenv = MatitaMisc.get_proof_metasenv status in
296 let context = MatitaMisc.get_proof_context status in
297 let aliases = MatitaMisc.get_proof_aliases status in
299 MatitaDisambiguator.disambiguate_term
300 dbd context metasenv 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
452 | Some f,_ -> Filename.basename f
453 | None,_ -> sprintf ".unnamed%d.ma" scriptId
456 ignore(GMain.Timeout.add ~ms:300000
457 ~callback:(fun _ -> self#_saveToBackuptFile ();true));
458 ignore(buffer#connect#modified_changed
459 (fun _ -> if buffer#modified then
460 set_star self#ppFilename true
462 set_star self#ppFilename false))
464 val mutable statements = []; (** executed statements *)
465 val mutable history = [ init ];
466 (** list of states before having executed statements. Head element of this
467 * list is the current state, last element is the state at the beginning of
469 * Invariant: this list length is 1 + length of statements *)
471 (** goal as seen by the user (i.e. metano corresponding to current tab) *)
472 val mutable userGoal = ~-1
474 (** text mark and tag representing locked part of a script *)
476 buffer#create_mark ~name:"locked" ~left_gravity:true buffer#start_iter
477 val locked_tag = buffer#create_tag [`BACKGROUND "lightblue"; `EDITABLE false]
478 val error_tag = buffer#create_tag [`UNDERLINE `SINGLE; `FOREGROUND "red"]
480 method locked_mark = locked_mark
481 method locked_tag = locked_tag
483 (* history can't be empty, the invariant above grant that it contains at
484 * least the init status *)
485 method status = match history with hd :: _ -> hd | _ -> assert false
487 method private _advance ?statement () =
488 let s = match statement with Some s -> s | None -> self#getFuture in
489 MatitaLog.debug ("evaluating: " ^ first_line s ^ " ...");
490 let (entries, parsed_len) =
491 eval_statement (buffer#get_iter_at_mark (`MARK locked_mark))#offset 0
492 error_tag buffer guistuff self#status userGoal self s
494 let (new_statuses, new_statements) = List.split entries in
495 history <- List.rev new_statuses @ history;
496 statements <- List.rev new_statements @ statements;
497 let start = buffer#get_iter_at_mark (`MARK locked_mark) in
498 let new_text = String.concat "" new_statements in
499 if statement <> None then
500 buffer#insert ~iter:start new_text
502 if new_text <> String.sub s 0 parsed_len then
504 let stop = start#copy#forward_chars parsed_len in
505 buffer#delete ~start ~stop;
506 buffer#insert ~iter:start new_text;
508 self#moveMark (String.length new_text)
510 method private _retract offset status new_statements new_history =
511 let cur_status = match history with s::_ -> s | [] -> assert false in
512 MatitaSync.time_travel ~present:cur_status ~past:status;
513 statements <- new_statements;
514 history <- new_history;
515 self#moveMark (- offset)
517 method advance ?statement () =
519 self#_advance ?statement ();
522 | Margin -> self#notify
523 | exc -> self#notify; raise exc
527 let cmp,new_statements,new_history,status =
528 match statements,history with
529 stat::statements, _::(status::_ as history) ->
530 String.length stat, statements, history, status
531 | [],[_] -> raise Margin
532 | _,_ -> assert false
534 self#_retract cmp status new_statements new_history;
537 | Margin -> self#notify
538 | exc -> self#notify; raise exc
540 method private getFuture =
541 buffer#get_text ~start:(buffer#get_iter_at_mark (`MARK locked_mark))
542 ~stop:buffer#end_iter ()
545 (** @param rel_offset relative offset from current position of locked_mark *)
546 method private moveMark rel_offset =
547 let mark = `MARK locked_mark in
548 let old_insert = buffer#get_iter_at_mark `INSERT in
549 buffer#remove_tag locked_tag ~start:buffer#start_iter ~stop:buffer#end_iter;
550 let current_mark_pos = buffer#get_iter_at_mark mark in
552 match rel_offset with
553 | 0 -> current_mark_pos
554 | n when n > 0 -> current_mark_pos#forward_chars n
555 | n (* when n < 0 *) -> current_mark_pos#backward_chars (abs n)
557 buffer#move_mark mark ~where:new_mark_pos;
558 buffer#apply_tag locked_tag ~start:buffer#start_iter ~stop:new_mark_pos;
559 buffer#move_mark `INSERT old_insert;
561 match self#status.proof_status with
562 Incomplete_proof (_,goal) -> self#setGoal goal
565 let mark_position = buffer#get_iter_at_mark mark in
566 if source_view#move_mark_onscreen mark then
568 buffer#move_mark mark mark_position;
569 source_view#scroll_to_mark ~use_align:true ~xalign:1.0 ~yalign:0.1 mark;
571 while Glib.Main.pending () do ignore(Glib.Main.iteration false); done
573 method clean_dirty_lock =
574 let lock_mark_iter = buffer#get_iter_at_mark (`MARK locked_mark) in
575 buffer#remove_tag locked_tag ~start:buffer#start_iter ~stop:buffer#end_iter;
576 buffer#apply_tag locked_tag ~start:buffer#start_iter ~stop:lock_mark_iter
578 val mutable observers = []
580 method addObserver (o: MatitaTypes.status -> unit) =
581 observers <- o :: observers
583 method private notify =
584 let status = self#status in
585 List.iter (fun o -> o status) observers
587 method loadFromFile f =
588 buffer#set_text (MatitaMisc.input_file f);
590 buffer#set_modified false
592 method assignFileName file =
593 let abspath = MatitaMisc.absolute_path file in
594 let devel = MatitamakeLib.development_for_dir (Filename.dirname abspath) in
595 guistuff.filenamedata <- Some abspath, devel
597 method saveToFile () =
598 let oc = open_out self#getFilename in
599 output_string oc (buffer#get_text ~start:buffer#start_iter
600 ~stop:buffer#end_iter ());
602 buffer#set_modified false
604 method private _saveToBackuptFile () =
605 if buffer#modified then
607 let f = self#ppFilename ^ "~" in
608 let oc = open_out f in
609 output_string oc (buffer#get_text ~start:buffer#start_iter
610 ~stop:buffer#end_iter ());
612 MatitaLog.debug ("backup " ^ f ^ " saved")
615 method private goto_top =
616 MatitaSync.time_travel ~present:self#status ~past:init
618 method private reset_buffer =
623 buffer#remove_tag locked_tag ~start:buffer#start_iter ~stop:buffer#end_iter;
624 buffer#move_mark (`MARK locked_mark) ~where:buffer#start_iter
628 source_buffer#begin_not_undoable_action ();
629 buffer#delete ~start:buffer#start_iter ~stop:buffer#end_iter;
630 source_buffer#end_not_undoable_action ();
631 buffer#set_modified false
634 let template = MatitaMisc.input_file BuildTimeConf.script_template in
635 buffer#insert ~iter:(buffer#get_iter `START) template;
636 guistuff.filenamedata <-
637 (None,MatitamakeLib.development_for_dir (Unix.getcwd ()));
638 buffer#set_modified false;
639 set_star self#ppFilename false
641 method goto (pos: [`Top | `Bottom | `Cursor]) () =
642 let old_locked_mark =
644 (buffer#create_mark ~name:"old_locked_mark"
645 ~left_gravity:true (buffer#get_iter_at_mark (`MARK locked_mark))) in
646 let getpos _ = buffer#get_iter_at_mark (`MARK locked_mark) in
647 let getoldpos _ = buffer#get_iter_at_mark old_locked_mark in
648 let dispose_old_locked_mark () = buffer#delete_mark old_locked_mark in
651 dispose_old_locked_mark ();
659 let newpos = getpos () in
660 if (getoldpos ())#compare newpos < 0 then
662 buffer#move_mark old_locked_mark newpos;
667 dispose_old_locked_mark ();
670 | Margin -> dispose_old_locked_mark (); self#notify
671 | exc -> dispose_old_locked_mark (); self#notify; raise exc)
673 let locked_iter () = buffer#get_iter_at_mark (`NAME "locked") in
674 let cursor_iter () = buffer#get_iter_at_mark `INSERT in
677 (buffer#create_mark ~name:"initial_insert"
678 ~left_gravity:true (cursor_iter ())) in
679 let dispose_remember () = buffer#delete_mark remember in
680 let remember_iter () =
681 buffer#get_iter_at_mark (`NAME "initial_insert") in
682 let cmp () = (locked_iter ())#offset - (remember_iter ())#offset in
684 let forward_until_cursor () = (* go forward until locked > cursor *)
687 if cmp () < 0 && (getoldpos ())#compare (getpos ()) < 0
690 buffer#move_mark old_locked_mark (getpos ());
696 let rec back_until_cursor len = (* go backward until locked < cursor *)
698 statements, (status::_ as history) when len <= 0 ->
699 self#_retract (icmp - len) status statements history
700 | statement::tl1, _::tl2 ->
701 back_until_cursor (len - String.length statement) (tl1,tl2)
702 | _,_ -> assert false
706 if icmp < 0 then (* locked < cursor *)
707 (forward_until_cursor (); self#notify)
708 else if icmp > 0 then (* locked > cursor *)
709 (back_until_cursor icmp (statements,history); self#notify)
710 else (* cursor = locked *)
714 dispose_old_locked_mark ();
716 | Margin -> dispose_remember (); dispose_old_locked_mark (); self#notify
717 | exc -> dispose_remember (); dispose_old_locked_mark ();
718 self#notify; raise exc)
720 method onGoingProof () =
721 match self#status.proof_status with
722 | No_proof | Proof _ -> false
723 | Incomplete_proof _ -> true
724 | Intermediate _ -> assert false
726 method proofStatus = MatitaMisc.get_proof_status self#status
727 method proofMetasenv = MatitaMisc.get_proof_metasenv self#status
728 method proofContext = MatitaMisc.get_proof_context self#status
729 method proofConclusion = MatitaMisc.get_proof_conclusion self#status
730 method setGoal n = userGoal <- n
733 let s = self#getFuture in
734 let rec is_there_and_executable s =
735 if Pcre.pmatch ~rex:only_dust_RE s then raise Margin;
736 let st = GrafiteParser.parse_statement (Stream.of_string s) in
738 | GrafiteAst.Comment (loc,_)->
739 let parsed_text_length = snd (CicNotationPt.loc_of_floc loc) in
740 let remain_len = String.length s - parsed_text_length in
741 let next = String.sub s parsed_text_length remain_len in
742 is_there_and_executable next
743 | GrafiteAst.Executable (loc, ex) -> false
746 is_there_and_executable s
748 | CicNotationParser.Parse_error _ -> false
755 MatitaLog.debug "script status:";
756 MatitaLog.debug ("history size: " ^ string_of_int (List.length history));
757 MatitaLog.debug (sprintf "%d statements:" (List.length statements));
758 List.iter MatitaLog.debug statements;
759 MatitaLog.debug ("Current file name: " ^
760 (match guistuff.filenamedata with
761 |None,_ -> "[ no name ]"
766 let _script = ref None
768 let script ~source_view ~init ~mathviewer ~urichooser ~develcreator ~ask_confirmation ~set_star ()
771 ~source_view ~init ~mathviewer ~ask_confirmation ~urichooser ~develcreator ~set_star ()
776 let instance () = match !_script with None -> assert false | Some s -> s