X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaScript.ml;h=c14bd77101628212a200e1066d31252c9c9792b5;hb=6a149d262dfcb03a7d57f8ecabf23b0b59e99f85;hp=49c3046b8eafeeaf74d0ccaa89635ac1df1289d4;hpb=c307d27343fe48aeeb2e1763a811f8122ac1c0df;p=helm.git

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index 49c3046b8..c14bd7710 100644
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -24,7 +24,7 @@
  *)
 
 open Printf
-open MatitaTypes
+open GrafiteTypes
 
 module TA = GrafiteAst
 
@@ -83,6 +83,9 @@ let eval_with_engine guistuff status user_goal parsed_text st =
         | None -> []
         | Some devel -> [MatitamakeLib.root_for_development devel ]
   in
+  let include_ =
+    include_ @ (Helm_registry.get_list Helm_registry.string "matita.includes")
+  in
   let parsed_text_length = String.length parsed_text in
   let loc, ex = 
     match st with TA.Executable (loc,ex) -> loc, ex | _ -> assert false in
@@ -98,7 +101,7 @@ let eval_with_engine guistuff status user_goal parsed_text st =
 (*     | Incomplete_proof { stack = stack }
       when not (List.mem user_goal (Continuationals.head_goals stack)) ->
         let status =
-          MatitaEngine.eval_ast ~include_paths:include_
+          MatitaEngine.eval_ast
             ~do_heavy_checks:true status (goal_ast user_goal)
         in
         let initial_space = if initial_space = "" then "\n" else initial_space
@@ -108,8 +111,11 @@ let eval_with_engine guistuff status user_goal parsed_text st =
           initial_space ^ TAPp.pp_tactical (TA.Select (loc, [user_goal])) ] *)
       | _ -> initial_space,status,[] in
   let new_status = 
-    MatitaEngine.eval_ast 
-      ~include_paths:include_ ~do_heavy_checks:true new_status st 
+    GrafiteEngine.eval_ast
+      ~baseuri_of_script:(GrafiteParserMisc.baseuri_of_script ~include_paths:include_)
+      ~disambiguate_tactic:GrafiteDisambiguate.disambiguate_tactic
+      ~disambiguate_command:GrafiteDisambiguate.disambiguate_command
+      ~do_heavy_checks:true new_status st 
   in
   let new_aliases =
     match ex with
@@ -126,13 +132,14 @@ let eval_with_engine guistuff status user_goal parsed_text st =
   let initial_space,status,new_status_and_text_list_rev = 
     let module DTE = DisambiguateTypes.Environment in
     let module UM = UriManager in
+    let baseuri = GrafiteTypes.get_string_option new_status "baseuri" in
     List.fold_left (
       fun (initial_space,status,acc) (k,((v,_) as value)) -> 
-        let b = 
-          try
-            let v = UM.strip_xpointer (UM.uri_of_string v) in
-            List.mem v new_status.objects 
-          with UM.IllFormedUri _ -> false
+        let b =
+         try
+          UM.buri_of_uri (UM.uri_of_string v) = baseuri
+         with
+          UriManager.IllFormedUri _ -> false (* v is a description, not a URI *)
         in
         if b then 
           initial_space,status,acc
@@ -160,8 +167,8 @@ let eval_with_engine guistuff status user_goal parsed_text st =
   try
     eval_with_engine guistuff status user_goal parsed_text st
   with
-  | MatitaEngine.UnableToInclude what 
-  | MatitaEngine.IncludedFileNotCompiled what as exc ->
+  | GrafiteParserMisc.UnableToInclude what 
+  | GrafiteEngine.IncludedFileNotCompiled what as exc ->
       let compile_needed_and_go_on d =
         let target = what in
         let refresh_cb () = 
@@ -214,8 +221,8 @@ let eval_with_engine guistuff status user_goal parsed_text st =
 let disambiguate_macro_term term status user_goal =
   let module MD = MatitaDisambiguator in
   let dbd = LibraryDb.instance () in
-  let metasenv = MatitaTypes.get_proof_metasenv status in
-  let context = MatitaTypes.get_proof_context status user_goal in
+  let metasenv = GrafiteTypes.get_proof_metasenv status in
+  let context = GrafiteTypes.get_proof_context status user_goal in
   let interps =
    MD.disambiguate_term ~dbd ~context ~metasenv ~aliases:status.aliases
     ~universe:(Some status.multi_aliases) term in
@@ -275,7 +282,7 @@ let eval_macro guistuff status user_goal unparsed_text parsed_text script mac =
       [], parsed_text_length
   (* REAL macro *)
   | TA.Hint loc -> 
-      let proof = MatitaTypes.get_current_proof status in
+      let proof = GrafiteTypes.get_current_proof status in
       let proof_status = proof, user_goal in
       let l = List.map fst (MQ.experimental_hint ~dbd proof_status) in
       let selected = guistuff.urichooser l in
@@ -289,7 +296,12 @@ let eval_macro guistuff status user_goal unparsed_text parsed_text script mac =
                 TA.Apply (loc, CicNotationPt.Uri (suri, None))),
                 Some (TA.Dot loc))))
           in
-        let new_status = MatitaEngine.eval_ast status ast in
+        let new_status =
+         GrafiteEngine.eval_ast
+          ~baseuri_of_script:(fun _ -> assert false)
+          ~disambiguate_tactic:GrafiteDisambiguate.disambiguate_tactic
+          ~disambiguate_command:GrafiteDisambiguate.disambiguate_command
+          status ast in
         let extra_text = 
           comment parsed_text ^ 
           "\n" ^ TAPp.pp_statement ast
@@ -303,8 +315,8 @@ let eval_macro guistuff status user_goal unparsed_text parsed_text script mac =
           ) selected;
           assert false)
   | TA.Check (_,term) ->
-      let metasenv = MatitaTypes.get_proof_metasenv status in
-      let context = MatitaTypes.get_proof_context status user_goal in
+      let metasenv = GrafiteTypes.get_proof_metasenv status in
+      let context = GrafiteTypes.get_proof_context status user_goal in
       let interps = 
         MatitaDisambiguator.disambiguate_term ~dbd ~context ~metasenv
          ~aliases:status.aliases ~universe:(Some status.multi_aliases) term
@@ -349,10 +361,10 @@ let eval_executable guistuff status user_goal unparsed_text parsed_text script
   match ex with
   | TA.Command (loc, _) | TA.Tactical (loc, _, _) ->
       (try 
-        (match MatitaMisc.baseuri_of_baseuri_decl (TA.Executable (loc,ex)) with
+        (match GrafiteParserMisc.baseuri_of_baseuri_decl (TA.Executable (loc,ex)) with
         | None -> ()
         | Some u -> 
-            if not (MatitaMisc.is_empty u) then
+            if not (GrafiteMisc.is_empty u) then
               match 
                 guistuff.ask_confirmation 
                   ~title:"Baseuri redefinition" 
@@ -366,8 +378,8 @@ let eval_executable guistuff status user_goal unparsed_text parsed_text script
                    LibraryClean.clean_baseuris ~basedir [u]
               | `NO -> ()
               | `CANCEL -> raise MatitaTypes.Cancel);
-        eval_with_engine 
-          guistuff status user_goal parsed_text (TA.Executable (loc, ex))
+        eval_with_engine
+         guistuff status user_goal parsed_text (TA.Executable (loc, ex))
       with MatitaTypes.Cancel -> [], 0)
   | TA.Macro (_,mac) ->
       eval_macro guistuff status user_goal unparsed_text parsed_text script mac
@@ -418,7 +430,6 @@ let fresh_script_id =
   fun () -> incr i; !i
 
 class script  ~(source_view: GSourceView.source_view)
-              ~(init: MatitaTypes.status) 
               ~(mathviewer: MatitaTypes.mathViewer) 
               ~set_star
               ~ask_confirmation
@@ -454,7 +465,7 @@ object (self)
       (fun _ -> set_star (Filename.basename self#ppFilename) buffer#modified))
 
   val mutable statements = [];    (** executed statements *)
-  val mutable history = [ init ];
+  val mutable history = [ MatitaSync.init () ];
     (** list of states before having executed statements. Head element of this
       * list is the current state, last element is the state at the beginning of
       * the script.
@@ -589,7 +600,7 @@ object (self)
 
   val mutable observers = []
 
-  method addObserver (o: MatitaTypes.status -> unit) =
+  method addObserver (o: GrafiteTypes.status -> unit) =
     observers <- o :: observers
 
   method private notify =
@@ -625,11 +636,20 @@ object (self)
       end
   
   method private goto_top =
+    let init = 
+      let rec last x = function 
+      | [] -> x
+      | hd::tl -> last hd tl
+      in
+      last self#status history
+    in
+    (* FIXME: this is not correct since there is no undo for 
+     * library_objects.set_default... *)
     MatitaSync.time_travel ~present:self#status ~past:init
 
   method private reset_buffer = 
     statements <- [];
-    history <- [ init ];
+    history <- [ MatitaSync.init () ];
     userGoal <- ~-1;
     self#notify;
     buffer#remove_tag locked_tag ~start:buffer#start_iter ~stop:buffer#end_iter;
@@ -640,7 +660,7 @@ object (self)
     source_buffer#begin_not_undoable_action ();
     buffer#delete ~start:buffer#start_iter ~stop:buffer#end_iter;
     source_buffer#end_not_undoable_action ();
-    buffer#set_modified false
+    buffer#set_modified false;
   
   method template () =
     let template = HExtlib.input_file BuildTimeConf.script_template in 
@@ -736,10 +756,10 @@ object (self)
     | Intermediate _ -> assert false
 
 (*   method proofStatus = MatitaTypes.get_proof_status self#status *)
-  method proofMetasenv = MatitaTypes.get_proof_metasenv self#status
-  method proofContext = MatitaTypes.get_proof_context self#status userGoal
-  method proofConclusion = MatitaTypes.get_proof_conclusion self#status userGoal
-  method stack = MatitaTypes.get_stack self#status
+  method proofMetasenv = GrafiteTypes.get_proof_metasenv self#status
+  method proofContext = GrafiteTypes.get_proof_context self#status userGoal
+  method proofConclusion= GrafiteTypes.get_proof_conclusion self#status userGoal
+  method stack = GrafiteTypes.get_stack self#status
   method setGoal n = userGoal <- n
   method goal = userGoal
 
@@ -777,10 +797,10 @@ end
 
 let _script = ref None
 
-let script ~source_view ~init ~mathviewer ~urichooser ~develcreator ~ask_confirmation ~set_star ()
+let script ~source_view ~mathviewer ~urichooser ~develcreator ~ask_confirmation ~set_star ()
 =
   let s = new script 
-    ~source_view ~init ~mathviewer ~ask_confirmation ~urichooser ~develcreator ~set_star () 
+    ~source_view ~mathviewer ~ask_confirmation ~urichooser ~develcreator ~set_star () 
   in
   _script := Some s;
   s