X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaScript.ml;h=ce613ef7180fd1fdc5b68d9779f338e462393446;hb=98e40a03f92d6715db7f53460e761455621346f2;hp=4f7027d61c83170577041400eafce92a5ea0a40e;hpb=6fa3a1e91d8a1e647775ca101255633ba265a9f2;p=helm.git diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml index 4f7027d61..ce613ef71 100644 --- a/helm/matita/matitaScript.ml +++ b/helm/matita/matitaScript.ml @@ -255,25 +255,28 @@ ask_confirmation user_goal parsed_text script ex = let module TA = TacticAst in let module TAPp = TacticAstPp in let module MD = MatitaDisambiguator in + let module ML = MatitacleanLib in let parsed_text_length = String.length parsed_text in match ex with | TA.Command (loc, _) | TA.Tactical (loc, _) -> - (match MatitacleanLib.baseuri_of_baseuri_decl (TA.Executable (loc,ex))with - | None -> () - | Some u -> - if not (MatitacleanLib.is_empty u) then - match - ask_confirmation - ~title:"Baseuri redefinition" - ~message:( - "Baseuri " ^ u ^ " already exists.\n" ^ - "Do you want to redefine the corresponding "^ - "part of the library?") - with - | `YES -> MatitacleanLib.clean_baseuris [u] - | `NO -> () - | `CANCEL -> raise MatitaTypes.Cancel); - eval_with_engine status user_goal parsed_text (TA.Executable (loc, ex)) + (try + (match ML.baseuri_of_baseuri_decl (TA.Executable (loc,ex)) with + | None -> () + | Some u -> + if not (MatitacleanLib.is_empty u) then + match + ask_confirmation + ~title:"Baseuri redefinition" + ~message:( + "Baseuri " ^ u ^ " already exists.\n" ^ + "Do you want to redefine the corresponding "^ + "part of the library?") + with + | `YES -> MatitacleanLib.clean_baseuris [u] + | `NO -> () + | `CANCEL -> raise MatitaTypes.Cancel); + eval_with_engine status user_goal parsed_text (TA.Executable (loc, ex)) + with MatitaTypes.Cancel -> [], 0) | TA.Macro (_,mac) -> eval_macro status mathviewer urichooser parsed_text script mac @@ -323,15 +326,15 @@ object (self) match filename with Some f -> f | None -> sprintf ".unnamed%d.ma" scriptId initializer - ignore(GMain.Timeout.add ~ms:30000 + ignore(GMain.Timeout.add ~ms:300000 ~callback:(fun _ -> self#_saveToBackuptFile ();true)); - set_star self#ppFilename false; ignore(buffer#connect#modified_changed (fun _ -> if buffer#modified then set_star self#ppFilename true else set_star self#ppFilename false)); - self#reset () + self#reset (); + self#template () val mutable statements = []; (** executed statements *) val mutable history = [ init ]; @@ -391,10 +394,19 @@ List.iter (fun s -> prerr_endline ("'" ^ s ^ "'")) new_statements; method advance ?statement () = try - self#_advance ?statement () - with Margin -> () + self#_advance ?statement (); + self#notify + with + | Margin -> self#notify + | exc -> self#notify; raise exc - method retract () = try self#_retract () with Margin -> () + method retract () = + try + self#_retract (); + self#notify + with + | Margin -> self#notify + | exc -> self#notify; raise exc method private getFuture = buffer#get_text ~start:(buffer#get_iter_at_mark (`MARK locked_mark)) @@ -415,7 +427,12 @@ List.iter (fun s -> prerr_endline ("'" ^ s ^ "'")) new_statements; buffer#move_mark mark ~where:new_mark_pos; buffer#apply_tag locked_tag ~start:buffer#start_iter ~stop:new_mark_pos; buffer#move_mark `INSERT old_insert; - self#notify + begin + match self#status.proof_status with + Incomplete_proof (_,goal) -> self#setGoal goal + | _ -> () + end ; + while Glib.Main.pending () do ignore(Glib.Main.iteration false); done val mutable observers = [] @@ -457,19 +474,38 @@ List.iter (fun s -> prerr_endline ("'" ^ s ^ "'")) new_statements; statements <- []; history <- [ init ]; userGoal <- ~-1; - self#notify; buffer#remove_tag locked_tag ~start:buffer#start_iter ~stop:buffer#end_iter; buffer#move_mark (`MARK locked_mark) ~where:buffer#start_iter method reset () = self#goto_top; - buffer#delete ~start:buffer#start_iter ~stop:buffer#end_iter + buffer#delete ~start:buffer#start_iter ~stop:buffer#end_iter; + self#notify; + buffer#set_modified false + + method template () = + let template = MatitaMisc.input_file BuildTimeConf.script_template in + buffer#insert ~iter:(buffer#get_iter `START) template; + filename <- None; + buffer#set_modified false; + set_star self#ppFilename false method goto (pos: [`Top | `Bottom | `Cursor]) () = match pos with - | `Top -> self#goto_top + | `Top -> self#goto_top; self#notify | `Bottom -> - (try while true do self#_advance () done with Margin -> ()) + (try + let getpos _ = buffer#get_iter_at_mark (`MARK locked_mark) in + let rec dowhile pos = + self#_advance (); + if pos#compare (getpos ()) < 0 then + dowhile (getpos ()) + in + dowhile (getpos ()); + self#notify + with + | Margin -> self#notify + | exc -> self#notify; raise exc) | `Cursor -> let locked_iter () = buffer#get_iter_at_mark (`NAME "locked") in let cursor_iter () = buffer#get_iter_at_mark `INSERT in @@ -486,13 +522,15 @@ List.iter (fun s -> prerr_endline ("'" ^ s ^ "'")) new_statements; let cmp = (locked_iter ())#compare (cursor_iter ()) in (try if cmp < 0 then (* locked < cursor *) - forward_until_cursor () + (forward_until_cursor (); self#notify) else if cmp > 0 then (* locked > cursor *) - back_until_cursor () + (back_until_cursor (); self#notify) else (* cursor = locked *) () - with Margin -> ()) - + with + | Margin -> self#notify + | exc -> self#notify; raise exc) + method onGoingProof () = match self#status.proof_status with | No_proof | Proof _ -> false @@ -504,6 +542,27 @@ List.iter (fun s -> prerr_endline ("'" ^ s ^ "'")) new_statements; method proofContext = MatitaMisc.get_proof_context self#status method setGoal n = userGoal <- n + method eos = + let s = self#getFuture in + let rec is_there_and_executable s = + if Pcre.pmatch ~rex:only_dust_RE s then raise Margin; + let st = CicTextualParser2.parse_statement (Stream.of_string s) in + match st with + | TacticAst.Comment (loc,_)-> + let parsed_text_length = snd (CicAst.loc_of_floc loc) in + let remain_len = String.length s - parsed_text_length in + let next = String.sub s parsed_text_length remain_len in + is_there_and_executable next + | TacticAst.Executable (loc, ex) -> false + in + try + is_there_and_executable s + with + | CicTextualParser2.Parse_error _ -> false + | Margin -> true + + + (* debug *) method dump () = MatitaLog.debug "script status:";