X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaEngine.ml;h=cb420d267ecf41f866a96dcb2695d1a95a93c00f;hb=b05dceab1903f9d15f214a9ddeaf791cd594e215;hp=17532cc90f21469a2816c158c6a88b59380ac34b;hpb=29a3bd5d160f31873236c93a008a9e4fd31c305e;p=helm.git

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 17532cc90..cb420d267 100644
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -220,22 +220,19 @@ let generate_projections uri fields status =
   ) status projections
 
 (* to avoid a long list of recursive functions *)
-let eval_from_stream_greedy_ref = ref (fun _ _ _ -> assert false);;
+let eval_from_stream_ref = ref (fun _ _ _ -> assert false);;
  
 let eval_command status cmd =
   match cmd with
+  | TacticAst.Default (loc, what, uris) as cmd ->
+     LibraryObjects.set_default what uris;
+     {status with moo_content_rev =
+        (TacticAstPp.pp_command cmd ^ "\n") :: status.moo_content_rev}
   | TacticAst.Include (loc, path) ->
      let path = MatitaMisc.obj_file_of_script path in
      let stream = Stream.of_channel (open_in path) in
      let status = ref status in
-      (try
-        !eval_from_stream_greedy_ref status stream (fun _ _ -> ())
-       with
-         CicTextualParser2.Parse_error (floc,err) as exc ->
-          (* check for EOI *)
-          if Stream.peek stream = None then ()
-          else raise exc
-      );
+      !eval_from_stream_ref status stream (fun _ _ -> ());
       !status
   | TacticAst.Set (loc, name, value) -> 
       let value = 
@@ -264,7 +261,12 @@ let eval_command status cmd =
       let obj = Cic.Constant (name,Some bo,ty,[],[]) in
       MatitaSync.add_obj uri obj status
   | TacticAst.Coercion (loc, coercion) -> 
-      eval_coercion status coercion
+      let status = eval_coercion status coercion in
+      let moo_content_rev =
+       (TacticAstPp.pp_cic_command
+         (TacticAst.Coercion (CicAst.dummy_floc,coercion)) ^ ".\n") ::
+       status.moo_content_rev in
+      {status with moo_content_rev = moo_content_rev}
   | TacticAst.Alias (loc, spec) -> 
      let aliases =
       match spec with
@@ -538,13 +540,14 @@ and disambiguate_tacticals status tacticals =
   status, tacticals
   
 let disambiguate_command status = function
-  | TacticAst.Include (loc,path) as cmd  -> status,cmd
+  | TacticAst.Default _
+  | TacticAst.Alias _
+  | TacticAst.Include _ as cmd  -> status,cmd
   | TacticAst.Coercion (loc, term) ->
       let status, term = disambiguate_term status term in
       status, TacticAst.Coercion (loc,term)
   | (TacticAst.Set _ | TacticAst.Qed _ | TacticAst.Drop _ ) as cmd ->
       status, cmd
-  | TacticAst.Alias _ as x -> status, x
   | TacticAst.Obj (loc,obj) ->
       let status,obj = disambiguate_obj status obj in
        status, TacticAst.Obj (loc,obj)
@@ -586,7 +589,11 @@ let eval_from_stream status str cb =
   let stl = CicTextualParser2.parse_statements str in
   List.iter
    (fun ast -> cb !status ast;status := eval_ast !status ast) stl
+;;
 
+(* to avoid a long list of recursive functions *)
+eval_from_stream_ref := eval_from_stream;;
+  
 let eval_from_stream_greedy status str cb =
   while true do
     print_string "matita> ";
@@ -597,9 +604,6 @@ let eval_from_stream_greedy status str cb =
   done
 ;;
 
-(* to avoid a long list of recursive functions *)
-eval_from_stream_greedy_ref := eval_from_stream_greedy;;
-  
 let eval_string status str =
   eval_from_stream status (Stream.of_string str) (fun _ _ -> ())