alias declarations are now put in the .moo file.

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

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 852608d5147d5a5cea305e2c7defdd9c42b86758..2de254ab3472601bafc2b0f543ab554b1a1d59b3 100644 (file)
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -219,7 +219,7 @@ let generate_projections uri fields status =
          status
   ) status projections
  
-let eval_command status cmd =
+let eval_command output status cmd =
   match cmd with
   | TacticAst.Set (loc, name, value) -> 
       let value = 
@@ -250,7 +250,8 @@ let eval_command status cmd =
   | TacticAst.Coercion (loc, coercion) -> 
       eval_coercion status coercion
   | TacticAst.Alias (loc, spec) -> 
-     (match spec with
+     let status =
+      match spec with
       | TacticAst.Ident_alias (id,uri) -> 
           {status with aliases = 
             DisambiguateTypes.Environment.add 
@@ -267,7 +268,10 @@ let eval_command status cmd =
           {status with aliases = 
             DisambiguateTypes.Environment.add 
               (DisambiguateTypes.Num instance) 
-              (DisambiguateChoices.lookup_num_by_dsc desc) status.aliases })
+              (DisambiguateChoices.lookup_num_by_dsc desc) status.aliases }
+     in
+      output (TacticAstPp.pp_alias spec ^ ".\n");
+      status
   | TacticAst.Obj (loc,obj) ->
      let ext,name =
       match obj with
@@ -310,19 +314,19 @@ let eval_command status cmd =
           | Cic.CurrentProof _
           | Cic.Variable _ -> assert false
 
-let eval_executable status ex =
+let eval_executable output status ex =
   match ex with
   | TacticAst.Tactical (_, tac) -> eval_tactical status tac
-  | TacticAst.Command (_, cmd) -> eval_command status cmd
+  | TacticAst.Command (_, cmd) -> eval_command output status cmd
   | TacticAst.Macro (_, mac) -> 
       command_error (sprintf "The macro %s can't be in a script" 
         (TacticAstPp.pp_macro_cic mac))
 
 let eval_comment status c = status
             
-let eval status st =
+let eval output status st =
   match st with
-  | TacticAst.Executable (_,ex) -> eval_executable status ex
+  | TacticAst.Executable (_,ex) -> eval_executable output status ex
   | TacticAst.Comment (_,c) -> eval_comment status c
 
 let disambiguate_term status term =
@@ -566,26 +570,27 @@ let disambiguate_statement status statement =
         let status, ex = disambiguate_executable status ex in
         status, TacticAst.Executable (loc,ex)
   
-let eval_ast status ast =
+let eval_ast output status ast =
   let status,st = disambiguate_statement status ast in
   (* this disambiguation step should be deferred to support tacticals *)
-  eval status st
+  eval output status st
 
-let eval_from_stream status str cb =
+let eval_from_stream output status str cb =
   let stl = CicTextualParser2.parse_statements str in
-  List.iter (fun ast -> cb !status ast;status := eval_ast !status ast) stl
+  List.iter
+   (fun ast -> cb !status ast;status := eval_ast output !status ast) stl
 
-let eval_from_stream_greedy status str cb =
+let eval_from_stream_greedy output status str cb =
   while true do
     print_string "matita> ";
     flush stdout;
     let ast = CicTextualParser2.parse_statement str in
     cb !status ast;
-    status := eval_ast !status ast 
+    status := eval_ast output !status ast 
   done
   
-let eval_string status str =
-  eval_from_stream status (Stream.of_string str) (fun _ _ -> ())
+let eval_string output status str =
+  eval_from_stream output status (Stream.of_string str) (fun _ _ -> ())
 
 let default_options () =
 (*