New command default "foo" uri1 ... urin

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

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index df8f484ba211a6f327614e805cd8f9f7d1ae19cf..cb420d267ecf41f866a96dcb2695d1a95a93c00f 100644 (file)
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -224,6 +224,10 @@ 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
@@ -536,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)