alias declarations are now put in the .moo file.

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

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index bd526212e45f9d7f88988f2ccb88341512dd9d5b..92fc2e42c47f0fd9c2f8d8373884a1c9ed1110df 100644 (file)
--- 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
@@ -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,8 +287,8 @@ 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
@@ -339,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";