"include" command implemented.

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

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index bd526212e45f9d7f88988f2ccb88341512dd9d5b..83aa603626a7300bf81a6146e97b0f3f67466cd2 100644 (file)
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -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 status (mathviewer:MatitaTypes.mathViewer) urichooser
+ parsed_text script mac
 =
   let module TA = TacticAst in
   let module TAPp = TacticAstPp in
@@ -192,10 +192,10 @@ 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 extra_text = 
@@ -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 status user_goal parsed_text
+       (TA.Executable (loc, ex))
   | TA.Macro (_,mac) ->
       eval_macro status mathviewer urichooser parsed_text script mac
 
-let rec eval_statement status (mathviewer:MatitaTypes.mathViewer) urichooser
-user_goal script s =
+let rec eval_statement 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 =
@@ -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 status mathviewer urichooser user_goal
+        parsed_text script ex
   
 let fresh_script_id =
   let i = ref 0 in