"include" command implemented.

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

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index 92fc2e42c47f0fd9c2f8d8373884a1c9ed1110df..83aa603626a7300bf81a6146e97b0f3f67466cd2 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 output status user_goal parsed_text st =
+let eval_with_engine 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 output status user_goal parsed_text st =
     match status.proof_status with
       | Incomplete_proof (_, goal) when goal <> user_goal ->
           goal_changed := true;
-          MatitaEngine.eval_ast output status (goal_ast user_goal)
+          MatitaEngine.eval_ast status (goal_ast user_goal)
       | _ -> status
   in
-  let new_status = MatitaEngine.eval_ast output status st in
+  let new_status = MatitaEngine.eval_ast status st in
   let new_aliases =
     match ex with
       | TA.Command (_, TA.Alias _) ->
@@ -133,7 +133,7 @@ let disambiguate term status =
   | [_,_,x,_] -> x
   | _ -> assert false
  
-let eval_macro output status (mathviewer:MatitaTypes.mathViewer) urichooser
+let eval_macro status (mathviewer:MatitaTypes.mathViewer) urichooser
  parsed_text script mac
 =
   let module TA = TacticAst in
@@ -197,7 +197,7 @@ let eval_macro output status (mathviewer:MatitaTypes.mathViewer) urichooser
             TA.Tactic (loc,
              TA.Apply (loc, CicAst.Uri (UriManager.string_of_uri uri,None))))))
         in
-        let new_status = MatitaEngine.eval_ast output status ast in
+        let new_status = MatitaEngine.eval_ast status ast in
         let extra_text = 
           comment parsed_text ^ 
           "\n" ^ TAPp.pp_statement ast
@@ -250,7 +250,7 @@ let eval_macro output status (mathviewer:MatitaTypes.mathViewer) urichooser
   | TA.Search_term (_, search_kind, term) -> failwith "not implemented"
 
                                 
-let eval_executable output status (mathviewer:MatitaTypes.mathViewer) urichooser
+let eval_executable status (mathviewer:MatitaTypes.mathViewer) urichooser
 user_goal parsed_text script ex =
   let module TA = TacticAst in
   let module TAPp = TacticAstPp in
@@ -258,12 +258,12 @@ 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 output status user_goal parsed_text
+      eval_with_engine status user_goal parsed_text
        (TA.Executable (loc, ex))
   | TA.Macro (_,mac) ->
-      eval_macro output status mathviewer urichooser parsed_text script mac
+      eval_macro status mathviewer urichooser parsed_text script mac
 
-let rec eval_statement output status (mathviewer:MatitaTypes.mathViewer)
+let rec eval_statement status (mathviewer:MatitaTypes.mathViewer)
  urichooser user_goal script s
 =
   if Pcre.pmatch ~rex:only_dust_RE s then raise Margin;
@@ -279,7 +279,7 @@ let rec eval_statement output status (mathviewer:MatitaTypes.mathViewer)
       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 output status mathviewer urichooser user_goal script s 
+        eval_statement status mathviewer urichooser user_goal script s 
       in
       (match s with
       | (status, text) :: tl ->
@@ -287,7 +287,7 @@ let rec eval_statement output status (mathviewer:MatitaTypes.mathViewer)
       | [] -> [], 0)
   | TacticAst.Executable (loc, ex) ->
       let parsed_text, parsed_text_length = text_of_loc loc in
-       eval_executable output status mathviewer urichooser user_goal
+       eval_executable status mathviewer urichooser user_goal
         parsed_text script ex
   
 let fresh_script_id =
@@ -341,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 (assert false) self#status mathviewer urichooser userGoal self s in
+      eval_statement self#status mathviewer urichooser userGoal self s in
     let (new_statuses, new_statements) = List.split entries in
 (*
 prerr_endline "evalStatement returned";