- commented out no longer needed macros Redo, Undo, Abort

[helm.git] / helm / matita / matitaScript.ml

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index 0d59d6f47fcfc9ba8b8e4031658bf382fcfe76dd..c8fbba9bee8a66c777ff205cb0d351aef5841ff4 100644 (file)
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -100,7 +100,7 @@ let eval_with_engine status user_goal parsed_text st =
     else
       new_text
   in
-    [ new_status, new_text ], parsed_text_length, None
+    [ new_status, new_text ], parsed_text_length
 
 let disambiguate term status =
   let module MD = MatitaDisambiguator in
@@ -114,7 +114,8 @@ let disambiguate term status =
   | _ -> assert false
  
 let eval_macro status (mathviewer:MatitaTypes.mathViewer) urichooser parsed_text
-script mac =
+  script mac
+=
   let module TA = TacticAst in
   let module TAPp = TacticAstPp in
   let module MQ = MetadataQuery in
@@ -132,18 +133,18 @@ script mac =
       let l =  MQ.match_term ~dbd term in
       let entry = `Whelp (TAPp.pp_macro_cic (TA.WMatch (loc, term)), l) in
       mathviewer#show_uri_list ~reuse:true ~entry l;
-      [], parsed_text_length, None
+      [], parsed_text_length
   | TA.WInstance (loc, term) ->
       let term = disambiguate term status in
       let l = MQ.instance ~dbd term in
       let entry = `Whelp (TAPp.pp_macro_cic (TA.WInstance (loc, term)), l) in
       mathviewer#show_uri_list ~reuse:true ~entry l;
-      [], parsed_text_length, None
+      [], parsed_text_length
   | TA.WLocate (loc, s) -> 
       let l = MQ.locate ~dbd s in
       let entry = `Whelp (TAPp.pp_macro_cic (TA.WLocate (loc, s)), l) in
       mathviewer#show_uri_list ~reuse:true ~entry l;
-      [], parsed_text_length, None  
+      [], parsed_text_length
   | TA.WElim (loc, term) ->
       let term = disambiguate term status in
       let uri =
@@ -154,21 +155,21 @@ script mac =
       let l = MQ.elim ~dbd uri in
       let entry = `Whelp (TAPp.pp_macro_cic (TA.WElim (loc, term)), l) in
       mathviewer#show_uri_list ~reuse:true ~entry l;
-      [], parsed_text_length, None  
+      [], parsed_text_length
   | TA.WHint (loc, term) ->
       let term = disambiguate term status in
       let s = ((None,[0,[],term], Cic.Meta (0,[]) ,term),0) in
       let l = List.map fst (MQ.experimental_hint ~dbd s) in
       let entry = `Whelp (TAPp.pp_macro_cic (TA.WHint (loc, term)), l) in
       mathviewer#show_uri_list ~reuse:true ~entry l;
-      [], parsed_text_length, None  
+      [], parsed_text_length
   (* REAL macro *)
   | TA.Hint loc -> 
       let s = MatitaMisc.get_proof_status status in
       let l = List.map fst (MQ.experimental_hint ~dbd s) in
       let selected = urichooser l in
       (match selected with
-      | [] -> [], parsed_text_length, None
+      | [] -> [], parsed_text_length
       | [uri] -> 
         let ast = 
           (TA.Executable (loc,
@@ -181,7 +182,7 @@ script mac =
           comment parsed_text ^ 
           "\n" ^ TAPp.pp_statement ast
         in
-        [ new_status , extra_text ], parsed_text_length, None
+        [ new_status , extra_text ], parsed_text_length
       | _ -> assert false)
   | TA.Check (_,term) ->
       let metasenv = MatitaMisc.get_proof_metasenv status in
@@ -199,8 +200,8 @@ script mac =
       let ty,_ = CTC.type_of_aux' metasenv context term ugraph in
       let t_and_ty = Cic.Cast (term,ty) in
       mathviewer#show_entry (`Cic (t_and_ty,metasenv));
-      [], parsed_text_length, None
-  | TA.Abort _ -> 
+      [], parsed_text_length
+(*   | TA.Abort _ -> 
       let rec go_back () =
         let status = script#status.proof_status in
         match status with
@@ -215,7 +216,7 @@ script mac =
   | TA.Undo (_, Some i) ->  [], parsed_text_length, 
       Some (fun () -> for j = 1 to i do script#retract () done)
   | TA.Undo (_, None) -> [], parsed_text_length, 
-      Some (fun () -> script#retract ())
+      Some (fun () -> script#retract ()) *)
   (* TODO *)
   | TA.Quit _ -> failwith "not implemented"
   | TA.Print (_,kind) -> failwith "not implemented"
@@ -249,13 +250,13 @@ user_goal script s =
       let parsed_text, parsed_text_length = text_of_loc loc in
       let remain_len = String.length s - parsed_text_length in
       let s = String.sub s parsed_text_length remain_len in
-      let s,len, act = 
+      let s,len = 
         eval_statement status mathviewer urichooser user_goal script s 
       in
       (match s with
       | (status, text) :: tl ->
-        ((status, parsed_text ^ text)::tl), (parsed_text_length + len), act
-      | [] -> [], 0, None)
+        ((status, parsed_text ^ text)::tl), (parsed_text_length + len)
+      | [] -> [], 0)
   | TacticAst.Executable (loc, ex) ->
       let parsed_text, parsed_text_length = text_of_loc loc in
       eval_executable 
@@ -290,7 +291,7 @@ object (self)
   method private _advance ?statement () =
     let s = match statement with Some s -> s | None -> self#getFuture in
     MatitaLog.debug ("evaluating: " ^ first_line s ^ " ...");
-    let (entries, parsed_len, post_advance_action) = 
+    let (entries, parsed_len) = 
       eval_statement self#status mathviewer urichooser userGoal self s in
     let (new_statuses, new_statements) = List.split entries in
 (*
@@ -306,10 +307,7 @@ List.iter (fun s -> prerr_endline ("'" ^ s ^ "'")) new_statements;
     end;
     let new_text = String.concat "" new_statements in
     buffer#insert ~iter:start new_text;
-    self#moveMark (String.length new_text);
-    match post_advance_action with 
-      | Some f -> f () 
-      | _ -> ()
+    self#moveMark (String.length new_text)
 
   method private _retract () =
     match statements, history with