X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaScript.ml;h=ffa356b536f1e3f9f437771089da85bc94c5629c;hb=18c6848695fbfa97508e0981f6875a6459429a58;hp=c35fb9307232975b1b8409005aea93bcc1810562;hpb=ebe70c001a623e0440f21cd16dc88f585edcf0ea;p=helm.git

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index c35fb9307..ffa356b53 100644
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -59,7 +59,7 @@ let first_line s =
   (** creates a statement AST for the Goal tactic, e.g. "goal 7" *)
 let goal_ast n =
   let module A = GrafiteAst in
-  let loc = DisambiguateTypes.dummy_floc in
+  let loc = HExtlib.dummy_floc in
   A.Executable (loc, A.Tactical (loc,
     A.Tactic (loc, A.Goal (loc, n)),
     Some (A.Dot loc)))
@@ -72,7 +72,9 @@ type guistuff = {
   mutable filenamedata: string option * MatitamakeLib.development option
 }
 
-let eval_with_engine guistuff status user_goal parsed_text st =
+let eval_with_engine guistuff lexicon_status grafite_status user_goal
+ parsed_text st
+=
   let module TAPp = GrafiteAstPp in
   let include_ = 
     match guistuff.filenamedata with
@@ -83,6 +85,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
@@ -92,45 +97,38 @@ let eval_with_engine guistuff status user_goal parsed_text st =
      pieces.(1), pieces.(2)
    with
     Not_found -> "", parsed_text in
-  (* we add the goal command if needed *)
-  let inital_space,new_status,new_status_and_text_list' =
-    match status.proof_status with
-(*     | Incomplete_proof { stack = stack }
+  let inital_space,new_grafite_status,new_lexicon_status,new_status_and_text_list' =
+   (* the code commented out adds the "select" command if needed *)
+   initial_space,grafite_status,lexicon_status,[] in
+(*    match grafite_status.proof_status with
+     | Incomplete_proof { stack = stack }
       when not (List.mem user_goal (Continuationals.head_goals stack)) ->
-        let status =
-          MatitaEngine.eval_ast ~include_paths:include_
-            ~do_heavy_checks:true status (goal_ast user_goal)
+        let grafite_status =
+          MatitaEngine.eval_ast
+            ~do_heavy_checks:true grafite_status (goal_ast user_goal)
         in
         let initial_space = if initial_space = "" then "\n" else initial_space
         in
-        "\n", status,
-        [ status,
-          initial_space ^ TAPp.pp_tactical (TA.Select (loc, [user_goal])) ] *)
-      | _ -> initial_space,status,[] in
-  let new_status = 
-    GrafiteEngine.eval_ast
-      ~disambiguate_tactic:GrafiteDisambiguate.disambiguate_tactic
-      ~disambiguate_command:GrafiteDisambiguate.disambiguate_command
-      ~include_paths:include_ ~do_heavy_checks:true new_status st 
+        "\n", grafite_status,
+        [ grafite_status,
+          initial_space ^ TAPp.pp_tactical (TA.Select (loc, [user_goal])) ]
+      | _ -> initial_space,grafite_status,[] in *)
+  let new_lexicon_status,new_grafite_status = 
+   MatitaEngine.eval_ast ~do_heavy_checks:true
+    new_lexicon_status new_grafite_status st
   in
   let new_aliases =
-    match ex with
-      | TA.Command (_, TA.Alias _)
-      | TA.Command (_, TA.Include _)
-      | TA.Command (_, TA.Interpretation _) -> []
-      | _ -> MatitaSync.alias_diff ~from:status new_status
-  in
+   LexiconSync.alias_diff ~from:lexicon_status new_lexicon_status in
   (* we remove the defined object since we consider them "automatic aliases" *)
   let dummy_st =
-    TA.Comment (DisambiguateTypes.dummy_floc,
-      TA.Note (DisambiguateTypes.dummy_floc, ""))
+    TA.Comment (HExtlib.dummy_floc, TA.Note (HExtlib.dummy_floc, ""))
   in
-  let initial_space,status,new_status_and_text_list_rev = 
+  let initial_space,lexicon_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
+    let baseuri = GrafiteTypes.get_string_option new_grafite_status "baseuri" in
     List.fold_left (
-      fun (initial_space,status,acc) (k,((v,_) as value)) -> 
+      fun (initial_space,lexicon_status,acc) (k,((v,_) as value)) -> 
         let b =
          try
           UM.buri_of_uri (UM.uri_of_string v) = baseuri
@@ -138,7 +136,7 @@ let eval_with_engine guistuff status user_goal parsed_text st =
           UriManager.IllFormedUri _ -> false (* v is a description, not a URI *)
         in
         if b then 
-          initial_space,status,acc
+          initial_space,lexicon_status,acc
         else
          let new_text =
           let initial_space =
@@ -147,23 +145,26 @@ let eval_with_engine guistuff status user_goal parsed_text st =
              DisambiguatePp.pp_environment
               (DisambiguateTypes.Environment.add k value
                 DisambiguateTypes.Environment.empty) in
-         let new_status =
-          MatitaSync.set_proof_aliases status [k,value]
+         let new_lexicon_status =
+          LexiconEngine.set_proof_aliases lexicon_status [k,value]
          in
-          "\n",new_status,((new_status, (new_text, dummy_st))::acc)
-    ) (initial_space,status,[]) new_aliases in
+          "\n",new_lexicon_status,(((new_grafite_status,new_lexicon_status), (new_text, Some dummy_st))::acc)
+    ) (initial_space,lexicon_status,[]) new_aliases in
   let parsed_text = initial_space ^ parsed_text in
   let res =
    List.rev new_status_and_text_list_rev @ new_status_and_text_list' @
-    [new_status, (parsed_text, st)]
+    [(new_grafite_status,new_lexicon_status),(parsed_text, Some st)]
   in
    res,parsed_text_length
 
-let eval_with_engine guistuff status user_goal parsed_text st =
+let eval_with_engine
+     guistuff lexicon_status grafite_status user_goal parsed_text st
+=
   try
-    eval_with_engine guistuff status user_goal parsed_text st
+   eval_with_engine guistuff lexicon_status grafite_status user_goal parsed_text
+    st
   with
-  | GrafiteEngine.UnableToInclude what 
+  | DependenciesParser.UnableToInclude what 
   | GrafiteEngine.IncludedFileNotCompiled what as exc ->
       let compile_needed_and_go_on d =
         let target = what in
@@ -173,7 +174,8 @@ let eval_with_engine guistuff status user_goal parsed_text st =
         if not(MatitamakeLib.build_development_in_bg ~target refresh_cb d) then
           raise exc
         else
-          eval_with_engine guistuff status user_goal parsed_text st
+         eval_with_engine guistuff lexicon_status grafite_status user_goal
+          parsed_text st
       in
       let do_nothing () = [], 0 in
       let handle_with_devel d =
@@ -214,19 +216,24 @@ let eval_with_engine guistuff status user_goal parsed_text st =
           | Some d -> handle_with_devel d
 ;;
 
-let disambiguate_macro_term term status user_goal =
-  let module MD = MatitaDisambiguator in
+let disambiguate_macro_term term lexicon_status grafite_status user_goal =
+  let module MD = GrafiteDisambiguator in
   let dbd = LibraryDb.instance () in
-  let metasenv = GrafiteTypes.get_proof_metasenv status in
-  let context = GrafiteTypes.get_proof_context status user_goal in
+  let metasenv = GrafiteTypes.get_proof_metasenv grafite_status in
+  let context = GrafiteTypes.get_proof_context grafite_status user_goal in
   let interps =
-   MD.disambiguate_term ~dbd ~context ~metasenv ~aliases:status.aliases
-    ~universe:(Some status.multi_aliases) term in
+   MD.disambiguate_term ~dbd ~context ~metasenv
+    ~aliases:lexicon_status.LexiconEngine.aliases
+    ~universe:(Some lexicon_status.LexiconEngine.multi_aliases) term in
   match interps with 
   | [_,_,x,_], _ -> x
   | _ -> assert false
+
+let pp_eager_statement_ast =
+  GrafiteAstPp.pp_statement ~term_pp:CicNotationPp.pp_term
+    ~lazy_term_pp:(fun _ -> assert false) ~obj_pp:(fun _ -> assert false)
  
-let eval_macro guistuff status user_goal unparsed_text parsed_text script mac =
+let eval_macro guistuff lexicon_status grafite_status user_goal unparsed_text parsed_text script mac =
   let module TAPp = GrafiteAstPp in
   let module MQ = MetadataQuery in
   let module MDB = LibraryDb in
@@ -235,10 +242,13 @@ let eval_macro guistuff status user_goal unparsed_text parsed_text script mac =
   (* no idea why ocaml wants this *)
   let parsed_text_length = String.length parsed_text in
   let dbd = LibraryDb.instance () in
+  (* XXX use a real CIC -> string pretty printer *)
+  let pp_macro = TAPp.pp_macro ~term_pp:CicPp.ppterm in
   match mac with
   (* WHELP's stuff *)
   | TA.WMatch (loc, term) -> 
-      let term = disambiguate_macro_term term status user_goal in
+      let term =
+       disambiguate_macro_term term lexicon_status grafite_status user_goal in
       let l =  Whelp.match_term ~dbd term in
       let query_url =
         MatitaMisc.strip_suffix ~suffix:"."
@@ -248,37 +258,40 @@ let eval_macro guistuff status user_goal unparsed_text parsed_text script mac =
       guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
       [], parsed_text_length
   | TA.WInstance (loc, term) ->
-      let term = disambiguate_macro_term term status user_goal in
+      let term =
+       disambiguate_macro_term term lexicon_status grafite_status user_goal in
       let l = Whelp.instance ~dbd term in
-      let entry = `Whelp (TAPp.pp_macro_cic (TA.WInstance (loc, term)), l) in
+      let entry = `Whelp (pp_macro (TA.WInstance (loc, term)), l) in
       guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
       [], parsed_text_length
   | TA.WLocate (loc, s) -> 
       let l = Whelp.locate ~dbd s in
-      let entry = `Whelp (TAPp.pp_macro_cic (TA.WLocate (loc, s)), l) in
+      let entry = `Whelp (pp_macro (TA.WLocate (loc, s)), l) in
       guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
       [], parsed_text_length
   | TA.WElim (loc, term) ->
-      let term = disambiguate_macro_term term status user_goal in
+      let term =
+       disambiguate_macro_term term lexicon_status grafite_status user_goal in
       let uri =
         match term with
         | Cic.MutInd (uri,n,_) -> UriManager.uri_of_uriref uri n None 
         | _ -> failwith "Not a MutInd"
       in
       let l = Whelp.elim ~dbd uri in
-      let entry = `Whelp (TAPp.pp_macro_cic (TA.WElim (loc, term)), l) in
+      let entry = `Whelp (pp_macro (TA.WElim (loc, term)), l) in
       guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
       [], parsed_text_length
   | TA.WHint (loc, term) ->
-      let term = disambiguate_macro_term term status user_goal in
+      let term =
+       disambiguate_macro_term term lexicon_status grafite_status user_goal in
       let s = ((None,[0,[],term], Cic.Meta (0,[]) ,term),0) in
       let l = List.map fst (MQ.experimental_hint ~dbd s) in
-      let entry = `Whelp (TAPp.pp_macro_cic (TA.WHint (loc, term)), l) in
+      let entry = `Whelp (pp_macro (TA.WHint (loc, term)), l) in
       guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
       [], parsed_text_length
   (* REAL macro *)
   | TA.Hint loc -> 
-      let proof = GrafiteTypes.get_current_proof status in
+      let proof = GrafiteTypes.get_current_proof grafite_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
@@ -292,16 +305,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 =
-         GrafiteEngine.eval_ast
-          ~disambiguate_tactic:GrafiteDisambiguate.disambiguate_tactic
-          ~disambiguate_command:GrafiteDisambiguate.disambiguate_command
-          status ast in
+        let new_lexicon_status,new_grafite_status =
+         MatitaEngine.eval_ast lexicon_status grafite_status ast in
         let extra_text = 
-          comment parsed_text ^ 
-          "\n" ^ TAPp.pp_statement ast
-        in
-        [ new_status , (extra_text, ast) ], parsed_text_length
+          comment parsed_text ^ "\n" ^ pp_eager_statement_ast ast in
+        [ (new_grafite_status,new_lexicon_status), (extra_text, Some ast) ],
+         parsed_text_length
       | _ -> 
           HLog.error 
             "The result of the urichooser should be only 1 uri, not:\n";
@@ -310,12 +319,12 @@ let eval_macro guistuff status user_goal unparsed_text parsed_text script mac =
           ) selected;
           assert false)
   | TA.Check (_,term) ->
-      let metasenv = GrafiteTypes.get_proof_metasenv status in
-      let context = GrafiteTypes.get_proof_context status user_goal in
+      let metasenv = GrafiteTypes.get_proof_metasenv grafite_status in
+      let context = GrafiteTypes.get_proof_context grafite_status user_goal in
       let interps = 
-        MatitaDisambiguator.disambiguate_term ~dbd ~context ~metasenv
-         ~aliases:status.aliases ~universe:(Some status.multi_aliases) term
-      in
+       GrafiteDisambiguator.disambiguate_term ~dbd ~context ~metasenv
+        ~aliases:lexicon_status.LexiconEngine.aliases
+        ~universe:(Some lexicon_status.LexiconEngine.multi_aliases) term in
       let _, metasenv , term, ugraph =
         match interps with 
         | [x], _ -> x
@@ -327,7 +336,7 @@ let eval_macro guistuff status user_goal unparsed_text parsed_text script mac =
       [], parsed_text_length
 (*   | TA.Abort _ -> 
       let rec go_back () =
-        let status = script#status.proof_status in
+        let grafite_status = script#grafite_status.proof_status in
         match status with
         | No_proof -> ()
         | _ -> script#retract ();go_back()
@@ -347,20 +356,23 @@ let eval_macro guistuff status user_goal unparsed_text parsed_text script mac =
   | TA.Search_pat (_, search_kind, str) -> failwith "not implemented"
   | TA.Search_term (_, search_kind, term) -> failwith "not implemented"
                                 
-let eval_executable guistuff status user_goal unparsed_text parsed_text script
-  ex
+let eval_executable guistuff lexicon_status grafite_status user_goal unparsed_text parsed_text script ex
 =
   let module TAPp = GrafiteAstPp in
-  let module MD = MatitaDisambiguator in
+  let module MD = GrafiteDisambiguator in
   let module ML = MatitaMisc in
   match ex with
-  | TA.Command (loc, _) | TA.Tactical (loc, _, _) ->
-      (try 
-        (match GrafiteMisc.baseuri_of_baseuri_decl (TA.Executable (loc,ex)) with
-        | None -> ()
-        | Some u -> 
+    TA.Tactical (loc, _, _) ->
+     eval_with_engine
+      guistuff lexicon_status grafite_status user_goal parsed_text
+       (TA.Executable (loc, ex))
+  | TA.Command (loc, cmd) ->
+     (try
+       begin
+        match cmd with
+         | TA.Set (loc',"baseuri",u) ->
             if not (GrafiteMisc.is_empty u) then
-              match 
+             (match 
                 guistuff.ask_confirmation 
                   ~title:"Baseuri redefinition" 
                   ~message:(
@@ -368,26 +380,33 @@ let eval_executable guistuff status user_goal unparsed_text parsed_text script
                     "Do you want to redefine the corresponding "^
                     "part of the library?")
               with
-              | `YES ->
-                  let basedir = Helm_registry.get "matita.basedir" in
-                   LibraryClean.clean_baseuris ~basedir [u]
-              | `NO -> ()
-              | `CANCEL -> raise MatitaTypes.Cancel);
-        eval_with_engine 
-          guistuff status user_goal parsed_text (TA.Executable (loc, ex))
-      with MatitaTypes.Cancel -> [], 0)
+               | `YES ->
+                   let basedir = Helm_registry.get "matita.basedir" in
+                    LibraryClean.clean_baseuris ~basedir [u]
+               | `NO -> ()
+               | `CANCEL -> raise MatitaTypes.Cancel)
+         | _ -> ()
+       end;
+       eval_with_engine
+        guistuff lexicon_status grafite_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
+      eval_macro guistuff lexicon_status grafite_status user_goal unparsed_text
+       parsed_text script mac
 
-let rec eval_statement (buffer : GText.buffer) guistuff status user_goal
- script statement
+let rec eval_statement (buffer : GText.buffer) guistuff lexicon_status
+ grafite_status user_goal script statement
 =
-  let st, unparsed_text =
+  let (lexicon_status,st), unparsed_text =
     match statement with
     | `Raw text ->
         if Pcre.pmatch ~rex:only_dust_RE text then raise Margin;
-        GrafiteParser.parse_statement (Ulexing.from_utf8_string text), text
-    | `Ast (st, text) -> st, text
+        GrafiteParser.parse_statement (Ulexing.from_utf8_string text)
+         ~include_paths:(Helm_registry.get_list
+           Helm_registry.string "matita.includes")
+         lexicon_status, text
+    | `Ast (st, text) -> (lexicon_status, st), text
   in
   let text_of_loc loc =
     let parsed_text_length = snd (HExtlib.loc_of_floc loc) in
@@ -395,37 +414,41 @@ let rec eval_statement (buffer : GText.buffer) guistuff status user_goal
     parsed_text, parsed_text_length
   in
   match st with
-  | GrafiteAst.Comment (loc, _) -> 
+  | GrafiteParser.LNone loc ->
+      let parsed_text, parsed_text_length = text_of_loc loc in
+       [(grafite_status,lexicon_status),(parsed_text,None)],
+        parsed_text_length
+  | GrafiteParser.LSome (GrafiteAst.Comment (loc, _)) -> 
       let parsed_text, parsed_text_length = text_of_loc loc in
       let remain_len = String.length unparsed_text - parsed_text_length in
       let s = String.sub unparsed_text parsed_text_length remain_len in
       let s,len = 
        try
-        eval_statement buffer guistuff status user_goal script
-         (`Raw s)
+        eval_statement buffer guistuff lexicon_status grafite_status user_goal
+         script (`Raw s)
        with
           HExtlib.Localized (floc, exn) ->
            HExtlib.raise_localized_exception ~offset:parsed_text_length floc exn
-        | MatitaDisambiguator.DisambiguationError (offset,errorll) ->
+        | GrafiteDisambiguator.DisambiguationError (offset,errorll) ->
            raise
-            (MatitaDisambiguator.DisambiguationError
+            (GrafiteDisambiguator.DisambiguationError
               (offset+parsed_text_length, errorll))
       in
       (match s with
-      | (status, (text, ast)) :: tl ->
-          ((status, (parsed_text ^ text, ast))::tl), (parsed_text_length + len)
+      | (statuses,(text, ast)) :: tl ->
+          (statuses,(parsed_text ^ text, ast))::tl,
+           parsed_text_length + len
       | [] -> [], 0)
-  | GrafiteAst.Executable (loc, ex) ->
+  | GrafiteParser.LSome (GrafiteAst.Executable (loc, ex)) ->
       let parsed_text, parsed_text_length = text_of_loc loc in
-      eval_executable guistuff status user_goal unparsed_text parsed_text
-        script ex 
+      eval_executable guistuff lexicon_status grafite_status user_goal
+       unparsed_text parsed_text script ex 
   
 let fresh_script_id =
   let i = ref 0 in
   fun () -> incr i; !i
 
 class script  ~(source_view: GSourceView.source_view)
-              ~(init: GrafiteTypes.status) 
               ~(mathviewer: MatitaTypes.mathViewer) 
               ~set_star
               ~ask_confirmation
@@ -434,6 +457,15 @@ class script  ~(source_view: GSourceView.source_view)
               () =
 let buffer = source_view#buffer in
 let source_buffer = source_view#source_buffer in
+let initial_statuses =
+ let include_paths =
+  Helm_registry.get_list Helm_registry.string "matita.includes" in
+ let lexicon_status =
+  CicNotation2.load_notation ~include_paths
+   BuildTimeConf.core_notation_script in
+ let grafite_status = GrafiteSync.init () in
+  grafite_status,lexicon_status
+in
 object (self)
   val scriptId = fresh_script_id ()
   
@@ -460,8 +492,9 @@ object (self)
     ignore (buffer#connect#modified_changed 
       (fun _ -> set_star (Filename.basename self#ppFilename) buffer#modified))
 
-  val mutable statements = [];    (** executed statements *)
-  val mutable history = [ init ];
+  val mutable statements = []    (** executed statements *)
+
+  val mutable history = [ initial_statuses ]
     (** 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.
@@ -481,13 +514,15 @@ object (self)
   method error_tag = error_tag
 
     (* history can't be empty, the invariant above grant that it contains at
-     * least the init status *)
-  method status = match history with hd :: _ -> hd | _ -> assert false
+     * least the init grafite_status *)
+  method grafite_status = match history with (s,_)::_ -> s | _ -> assert false
+  method lexicon_status = match history with (_,ss)::_ -> ss | _ -> assert false
 
   method private _advance ?statement () =
     let rec aux st =
       let (entries, parsed_len) = 
-        eval_statement buffer guistuff self#status userGoal self st
+        eval_statement buffer guistuff self#lexicon_status self#grafite_status
+         userGoal self st
       in
       let (new_statuses, new_statements, new_asts) =
         let statuses, statements = List.split entries in
@@ -499,41 +534,28 @@ object (self)
       let start = buffer#get_iter_at_mark (`MARK locked_mark) in
       let new_text = String.concat "" new_statements in
       if statement <> None then
-       buffer#insert ~iter:start new_text
-      else
+        buffer#insert ~iter:start new_text
+      else begin
         let s = match st with `Raw s | `Ast (_, s) -> s in
-        if new_text <> String.sub s 0 parsed_len then
-        begin
-          let stop = start#copy#forward_chars parsed_len in
-          buffer#delete ~start ~stop;
+        if new_text <> String.sub s 0 parsed_len then begin
+          buffer#delete ~start ~stop:(start#copy#forward_chars parsed_len);
           buffer#insert ~iter:start new_text;
         end;
-      self#moveMark (String.length new_text);
-      (*
-      (match List.rev new_asts with (* advance again on punctuation *)
-      | TA.Executable (_, TA.Tactical (_, tac, _)) :: _ ->
-          let baseoffset =
-            (buffer#get_iter_at_mark (`MARK locked_mark))#offset
-          in
-          let text = self#getFuture in
-          (try
-            (match parse_statement baseoffset 0 buffer text with
-            | TA.Executable (loc, TA.Tactical (_, tac, None)) as st
-              when GrafiteAst.is_punctuation tac ->
-                let len = snd (CicNotationPt.loc_of_floc loc) in
-                aux (`Ast (st, String.sub text 0 len))
-            | _ -> ())
-          with CicNotationParser.Parse_error _ | End_of_file -> ())
-      | _ -> ())
-      *)
+      end;
+      self#moveMark (String.length new_text)
     in
     let s = match statement with Some s -> s | None -> self#getFuture in
     HLog.debug ("evaluating: " ^ first_line s ^ " ...");
     (try aux (`Raw s) with End_of_file -> raise Margin)
 
-  method private _retract offset status new_statements new_history =
-    let cur_status = match history with s::_ -> s | [] -> assert false in
-    MatitaSync.time_travel ~present:cur_status ~past:status;
+  method private _retract offset lexicon_status grafite_status new_statements
+   new_history
+  =
+   let cur_grafite_status,cur_lexicon_status =
+    match history with s::_ -> s | [] -> assert false
+   in
+    LexiconSync.time_travel ~present:cur_lexicon_status ~past:lexicon_status;
+    GrafiteSync.time_travel ~present:cur_grafite_status ~past:grafite_status;
     statements <- new_statements;
     history <- new_history;
     self#moveMark (- offset)
@@ -548,14 +570,15 @@ object (self)
 
   method retract () =
     try
-      let cmp,new_statements,new_history,status =
+      let cmp,new_statements,new_history,(grafite_status,lexicon_status) =
        match statements,history with
           stat::statements, _::(status::_ as history) ->
            String.length stat, statements, history, status
        | [],[_] -> raise Margin
        | _,_ -> assert false
       in
-       self#_retract cmp status new_statements new_history;
+       self#_retract cmp lexicon_status grafite_status new_statements
+        new_history;
        self#notify
     with 
     | Margin -> self#notify
@@ -596,12 +619,13 @@ object (self)
 
   val mutable observers = []
 
-  method addObserver (o: GrafiteTypes.status -> unit) =
+  method addObserver (o: LexiconEngine.status -> GrafiteTypes.status -> unit) =
     observers <- o :: observers
 
   method private notify =
-    let status = self#status in
-    List.iter (fun o -> o status) observers
+    let lexicon_status = self#lexicon_status in
+    let grafite_status = self#grafite_status in
+    List.iter (fun o -> o lexicon_status grafite_status) observers
 
   method loadFromFile f =
     buffer#set_text (HExtlib.input_file f);
@@ -632,11 +656,21 @@ object (self)
       end
   
   method private goto_top =
-    MatitaSync.time_travel ~present:self#status ~past:init
+    let grafite_status,lexicon_status = 
+      let rec last x = function 
+      | [] -> x
+      | hd::tl -> last hd tl
+      in
+      last (self#grafite_status,self#lexicon_status) history
+    in
+    (* FIXME: this is not correct since there is no undo for 
+     * library_objects.set_default... *)
+    GrafiteSync.time_travel ~present:self#grafite_status ~past:grafite_status;
+    LexiconSync.time_travel ~present:self#lexicon_status ~past:lexicon_status
 
   method private reset_buffer = 
     statements <- [];
-    history <- [ init ];
+    history <- [ initial_statuses ];
     userGoal <- ~-1;
     self#notify;
     buffer#remove_tag locked_tag ~start:buffer#start_iter ~stop:buffer#end_iter;
@@ -647,7 +681,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 
@@ -714,8 +748,10 @@ object (self)
         in
         let rec back_until_cursor len = (* go backward until locked < cursor *)
          function
-            statements, (status::_ as history) when len <= 0 ->
-             self#_retract (icmp - len) status statements history
+            statements, ((grafite_status,lexicon_status)::_ as history)
+            when len <= 0 ->
+             self#_retract (icmp - len) lexicon_status grafite_status statements
+              history
           | statement::tl1, _::tl2 ->
              back_until_cursor (len - String.length statement) (tl1,tl2)
           | _,_ -> assert false
@@ -737,34 +773,42 @@ object (self)
                  self#notify; raise exc)
               
   method onGoingProof () =
-    match self#status.proof_status with
+    match self#grafite_status.proof_status with
     | No_proof | Proof _ -> false
     | Incomplete_proof _ -> true
     | Intermediate _ -> assert false
 
 (*   method proofStatus = MatitaTypes.get_proof_status 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 proofMetasenv = GrafiteTypes.get_proof_metasenv self#grafite_status
+  method proofContext =
+   GrafiteTypes.get_proof_context self#grafite_status userGoal
+  method proofConclusion =
+   GrafiteTypes.get_proof_conclusion self#grafite_status userGoal
+  method stack = GrafiteTypes.get_stack self#grafite_status
   method setGoal n = userGoal <- n
   method goal = userGoal
 
   method eos = 
     let s = self#getFuture in
-    let rec is_there_and_executable s = 
+    let rec is_there_and_executable lexicon_status s = 
       if Pcre.pmatch ~rex:only_dust_RE s then raise Margin;
-      let st = GrafiteParser.parse_statement (Ulexing.from_utf8_string s) in
+      let lexicon_status,st =
+       GrafiteParser.parse_statement (Ulexing.from_utf8_string s)
+        ~include_paths:(Helm_registry.get_list
+          Helm_registry.string "matita.includes")
+        lexicon_status
+      in
       match st with
-      | GrafiteAst.Comment (loc,_)-> 
+        GrafiteParser.LNone loc
+      | GrafiteParser.LSome (GrafiteAst.Comment (loc,_)) -> 
           let parsed_text_length = snd (HExtlib.loc_of_floc loc) in
           let remain_len = String.length s - parsed_text_length in
           let next = String.sub s parsed_text_length remain_len in
-          is_there_and_executable next
-      | GrafiteAst.Executable (loc, ex) -> false
+          is_there_and_executable lexicon_status next
+      | GrafiteParser.LSome (GrafiteAst.Executable (loc, ex)) -> false
     in
     try
-      is_there_and_executable s
+      is_there_and_executable self#lexicon_status s
     with 
     | CicNotationParser.Parse_error _ -> false
     | Margin | End_of_file -> true
@@ -784,10 +828,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