X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fmatita%2FmatitaScript.ml;h=92fc2e42c47f0fd9c2f8d8373884a1c9ed1110df;hb=6ec0a251ac681afb3a305323097d72ab80d7da6b;hp=c7859a7c7b96df61e8501b289d146237bc0b5709;hpb=a7b90d2494f7d580faa54ecd2835bd4649129763;p=helm.git diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml index c7859a7c7..92fc2e42c 100644 --- a/helm/matita/matitaScript.ml +++ b/helm/matita/matitaScript.ml @@ -65,7 +65,7 @@ let goal_ast n = let loc = CicAst.dummy_floc in A.Executable (loc, A.Tactical (loc, A.Tactic (loc, A.Goal (loc, n)))) -let eval_with_engine status user_goal parsed_text st = +let eval_with_engine output status user_goal parsed_text st = let module TA = TacticAst in let module TAPp = TacticAstPp in let parsed_text_length = String.length parsed_text in @@ -77,10 +77,10 @@ let eval_with_engine status user_goal parsed_text st = match status.proof_status with | Incomplete_proof (_, goal) when goal <> user_goal -> goal_changed := true; - MatitaEngine.eval_ast status (goal_ast user_goal) + MatitaEngine.eval_ast output status (goal_ast user_goal) | _ -> status in - let new_status = MatitaEngine.eval_ast status st in + let new_status = MatitaEngine.eval_ast output status st in let new_aliases = match ex with | TA.Command (_, TA.Alias _) -> @@ -133,8 +133,8 @@ let disambiguate term status = | [_,_,x,_] -> x | _ -> assert false -let eval_macro status (mathviewer:MatitaTypes.mathViewer) urichooser parsed_text - script mac +let eval_macro output status (mathviewer:MatitaTypes.mathViewer) urichooser + parsed_text script mac = let module TA = TacticAst in let module TAPp = TacticAstPp in @@ -169,7 +169,7 @@ let eval_macro status (mathviewer:MatitaTypes.mathViewer) urichooser parsed_text let term = disambiguate term status in let uri = match term with - | Cic.MutInd (uri,n,_) -> UriManager.uri_of_string (UriManager.string_of_uriref (uri,[n])) + | Cic.MutInd (uri,n,_) -> UriManager.uri_of_uriref uri n None | _ -> failwith "Not a MutInd" in let l = MQ.elim ~dbd uri in @@ -192,12 +192,12 @@ let eval_macro status (mathviewer:MatitaTypes.mathViewer) urichooser parsed_text | [] -> [], parsed_text_length | [uri] -> let ast = - (TA.Executable (loc, - (TA.Tactical (loc, - TA.Tactic (loc, - TA.Apply (loc, CicAst.Uri (UriManager.string_of_uri uri,None))))))) + TA.Executable (loc, + (TA.Tactical (loc, + TA.Tactic (loc, + TA.Apply (loc, CicAst.Uri (UriManager.string_of_uri uri,None)))))) in - let new_status = MatitaEngine.eval_ast status ast in + let new_status = MatitaEngine.eval_ast output status ast in let extra_text = comment parsed_text ^ "\n" ^ TAPp.pp_statement ast @@ -250,7 +250,7 @@ let eval_macro status (mathviewer:MatitaTypes.mathViewer) urichooser parsed_text | TA.Search_term (_, search_kind, term) -> failwith "not implemented" -let eval_executable status (mathviewer:MatitaTypes.mathViewer) urichooser +let eval_executable output status (mathviewer:MatitaTypes.mathViewer) urichooser user_goal parsed_text script ex = let module TA = TacticAst in let module TAPp = TacticAstPp in @@ -258,12 +258,14 @@ user_goal parsed_text script ex = let parsed_text_length = String.length parsed_text in match ex with | TA.Command (loc, _) | TA.Tactical (loc, _) -> - eval_with_engine status user_goal parsed_text (TA.Executable (loc, ex)) + eval_with_engine output status user_goal parsed_text + (TA.Executable (loc, ex)) | TA.Macro (_,mac) -> - eval_macro status mathviewer urichooser parsed_text script mac + eval_macro output status mathviewer urichooser parsed_text script mac -let rec eval_statement status (mathviewer:MatitaTypes.mathViewer) urichooser -user_goal script s = +let rec eval_statement output status (mathviewer:MatitaTypes.mathViewer) + urichooser user_goal script s += if Pcre.pmatch ~rex:only_dust_RE s then raise Margin; let st = CicTextualParser2.parse_statement (Stream.of_string s) in let text_of_loc loc = @@ -277,7 +279,7 @@ user_goal script s = let remain_len = String.length s - parsed_text_length in let s = String.sub s parsed_text_length remain_len in let s,len = - eval_statement status mathviewer urichooser user_goal script s + eval_statement output status mathviewer urichooser user_goal script s in (match s with | (status, text) :: tl -> @@ -285,15 +287,35 @@ user_goal script s = | [] -> [], 0) | TacticAst.Executable (loc, ex) -> let parsed_text, parsed_text_length = text_of_loc loc in - eval_executable - status mathviewer urichooser user_goal parsed_text script ex + eval_executable output status mathviewer urichooser user_goal + parsed_text script ex +let fresh_script_id = + let i = ref 0 in + fun () -> incr i; !i class script ~(buffer: GText.buffer) ~(init: MatitaTypes.status) ~(mathviewer: MatitaTypes.mathViewer) + ~set_star ~urichooser () = object (self) - initializer self#reset () + val mutable filename = None + val scriptId = fresh_script_id () + method private getFilename = + match filename with Some f -> f | _ -> assert false + method private ppFilename = + match filename with Some f -> f | None -> sprintf ".unnamed%d.ma" scriptId + + initializer + ignore(GMain.Timeout.add ~ms:30000 + ~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 () val mutable statements = []; (** executed statements *) val mutable history = [ init ]; @@ -305,6 +327,7 @@ object (self) (** goal as seen by the user (i.e. metano corresponding to current tab) *) val mutable userGoal = ~-1 + (** text mark and tag representing locked part of a script *) val locked_mark = buffer#create_mark ~name:"locked" ~left_gravity:true buffer#start_iter @@ -318,7 +341,7 @@ object (self) let s = match statement with Some s -> s | None -> self#getFuture in MatitaLog.debug ("evaluating: " ^ first_line s ^ " ..."); let (entries, parsed_len) = - eval_statement self#status mathviewer urichooser userGoal self s in + eval_statement (assert false) self#status mathviewer urichooser userGoal self s in let (new_statuses, new_statements) = List.split entries in (* prerr_endline "evalStatement returned"; @@ -327,12 +350,16 @@ List.iter (fun s -> prerr_endline ("'" ^ s ^ "'")) new_statements; history <- List.rev new_statuses @ history; statements <- List.rev new_statements @ statements; let start = buffer#get_iter_at_mark (`MARK locked_mark) in - if statement = None then begin - let stop = start#copy#forward_chars parsed_len in - buffer#delete ~start ~stop - end; let new_text = String.concat "" new_statements in - buffer#insert ~iter:start new_text; + if new_text <> String.sub s 0 parsed_len then + begin +(* prerr_endline ("new:" ^ new_text); *) +(* prerr_endline ("s:" ^ String.sub s 0 parsed_len); *) + let stop = start#copy#forward_chars parsed_len in + buffer#delete ~start ~stop; + buffer#insert ~iter:start new_text; +(* prerr_endline "AUTOMATICALLY MODIFIED!!!!!" *) + end; self#moveMark (String.length new_text) method private _retract () = @@ -381,16 +408,32 @@ List.iter (fun s -> prerr_endline ("'" ^ s ^ "'")) new_statements; let status = self#status in List.iter (fun o -> o status) observers - method loadFrom fname = - buffer#set_text (MatitaMisc.input_file fname); - self#goto_top - - method saveTo fname = - let oc = open_out fname in + method loadFromFile () = + buffer#set_text (MatitaMisc.input_file self#getFilename); + self#goto_top; + buffer#set_modified false + + method assignFileName file = + filename <- Some file; + + method saveToFile () = + let oc = open_out self#getFilename in output_string oc (buffer#get_text ~start:buffer#start_iter ~stop:buffer#end_iter ()); - close_out oc - + close_out oc; + buffer#set_modified false + + method private _saveToBackuptFile () = + if buffer#modified then + begin + let f = self#ppFilename ^ "~" in + let oc = open_out f in + output_string oc (buffer#get_text ~start:buffer#start_iter + ~stop:buffer#end_iter ()); + close_out oc; + MatitaLog.debug ("backup " ^ f ^ " saved") + end + method private goto_top = MatitaSync.time_travel ~present:self#status ~past:init; statements <- []; @@ -449,13 +492,15 @@ List.iter (fun s -> prerr_endline ("'" ^ s ^ "'")) new_statements; MatitaLog.debug ("history size: " ^ string_of_int (List.length history)); MatitaLog.debug (sprintf "%d statements:" (List.length statements)); List.iter MatitaLog.debug statements; + MatitaLog.debug ("Current file name: " ^ + (match filename with None -> "[ no name ]" | Some f -> f)); end let _script = ref None -let script ~buffer ~init ~mathviewer ~urichooser () = - let s = new script ~buffer ~init ~mathviewer ~urichooser () in +let script ~buffer ~init ~mathviewer ~urichooser ~set_star () = + let s = new script ~buffer ~init ~mathviewer ~urichooser ~set_star () in _script := Some s; s