]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/matita/matitaScript.ml
removed no longer used METAs
[helm.git] / helm / matita / matitaScript.ml
index 4413f9b8a3bbc0726c752a1cdd53fcafe564df71..188726d9510879720ff984782cd5d8e26fe558d6 100644 (file)
  * http://helm.cs.unibo.it/
  *)
 
+(* $Id$ *)
+
 open Printf
-open MatitaTypes
+open GrafiteTypes
 
 module TA = GrafiteAst
 
@@ -33,6 +35,8 @@ let debug_print = if debug then prerr_endline else ignore
 
   (** raised when one of the script margins (top or bottom) is reached *)
 exception Margin
+exception NoUnfinishedProof
+exception ActionCancelled
 
 let safe_substring s i j =
   try String.sub s i j with Invalid_argument _ -> assert false
@@ -59,7 +63,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,107 +76,89 @@ 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
-    | None,None -> []
-    | None,Some devel -> [MatitamakeLib.root_for_development devel ]
-    | Some f,_ -> 
-        match MatitamakeLib.development_for_dir (Filename.dirname f) with
-        | None -> []
-        | Some devel -> [MatitamakeLib.root_for_development devel ]
-  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
   let initial_space,parsed_text =
    try
     let pieces = Pcre.extract ~rex:heading_nl_RE' parsed_text in
      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
+(* let loc, ex = 
+    match st with TA.Executable (loc,ex) -> loc, ex | _ -> assert false 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 = 
-    MatitaEngine.eval_ast 
-      ~include_paths:include_ ~do_heavy_checks:true new_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
-  (* we remove the defined object since we consider them "automatic aliases" *)
-  let dummy_st =
-    TA.Comment (DisambiguateTypes.dummy_floc,
-      TA.Note (DisambiguateTypes.dummy_floc, ""))
+        "\n", grafite_status,
+        [ grafite_status,
+          initial_space ^ TAPp.pp_tactical (TA.Select (loc, [user_goal])) ]
+      | _ -> initial_space,grafite_status,[] in *)
+  let enriched_history_fragment =
+   MatitaEngine.eval_ast ~do_heavy_checks:true
+    new_lexicon_status new_grafite_status st
   in
-  let initial_space,status,new_status_and_text_list_rev = 
+  let _,new_text_list_rev = 
     let module DTE = DisambiguateTypes.Environment in
     let module UM = UriManager 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.exists (fun (s,_) -> s = v) new_status.objects 
-          with UM.IllFormedUri _ -> false
-        in
-        if b then 
-          initial_space,status,acc
-        else
-         let new_text =
-          let initial_space =
-           if initial_space = "" then "\n" else initial_space in
-            initial_space ^
-             DisambiguatePp.pp_environment
-              (DisambiguateTypes.Environment.add k value
-                DisambiguateTypes.Environment.empty) in
-         let new_status =
-          MatitaSync.set_proof_aliases status [k,value]
-         in
-          "\n",new_status,((new_status, (new_text, dummy_st))::acc)
-    ) (initial_space,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)]
+    List.fold_right (
+      fun (_,alias) (initial_space,acc) ->
+       match alias with
+          None -> initial_space,initial_space::acc
+        | Some (k,((v,_) as value)) ->
+           let new_text =
+            let initial_space =
+             if initial_space = "" then "\n" else initial_space
+            in
+             initial_space ^
+              DisambiguatePp.pp_environment
+               (DisambiguateTypes.Environment.add k value
+                 DisambiguateTypes.Environment.empty)
+           in
+            "\n",new_text::acc
+    ) enriched_history_fragment (initial_space,[]) in
+  let new_text_list_rev =
+   match enriched_history_fragment,new_text_list_rev with
+      (_,None)::_, initial_space::tl -> (initial_space ^ parsed_text)::tl
+    | _,_ -> assert false
   in
-   res,parsed_text_length
-
-let eval_with_engine guistuff status user_goal parsed_text st =
-  try
-    eval_with_engine guistuff status user_goal parsed_text st
+   let res =
+    try
+     List.combine (fst (List.split enriched_history_fragment)) new_text_list_rev
+    with
+     Invalid_argument _ -> assert false
+   in
+    res,parsed_text_length
+
+let wrap_with_developments guistuff f arg = 
+  try 
+    f arg
   with
-  | MatitaEngine.UnableToInclude what 
-  | MatitaEngine.IncludedFileNotCompiled what as exc ->
+  | DependenciesParser.UnableToInclude what 
+  | LexiconEngine.IncludedFileNotCompiled what 
+  | GrafiteEngine.IncludedFileNotCompiled what as exc ->
       let compile_needed_and_go_on d =
-        let target = what in
+        let target = Pcre.replace ~pat:"lexicon$" ~templ:"moo" what in
         let refresh_cb () = 
           while Glib.Main.pending () do ignore(Glib.Main.iteration false); done
         in
         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
+          f arg
       in
-      let do_nothing () = [], 0 in
+      let do_nothing () = raise ActionCancelled in
       let handle_with_devel d =
         let name = MatitamakeLib.name_for_development d in
         let title = "Unable to include " ^ what in
@@ -210,177 +196,175 @@ let eval_with_engine guistuff status user_goal parsed_text st =
           | None -> handle_without_devel (Some f)
           | Some d -> handle_with_devel d
 ;;
+    
+let eval_with_engine
+     guistuff lexicon_status grafite_status user_goal parsed_text st
+=
+  wrap_with_developments guistuff
+    (eval_with_engine 
+      guistuff lexicon_status grafite_status user_goal parsed_text) st
+;;
 
-let disambiguate_macro_term term status user_goal =
-  let module MD = MatitaDisambiguator in
-  let dbd = MatitaDb.instance () in
-  let metasenv = MatitaTypes.get_proof_metasenv status in
-  let context = MatitaTypes.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
-  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 rec eval_macro include_paths (buffer : GText.buffer) 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 = MatitaDb in
+  let module MDB = LibraryDb in
   let module CTC = CicTypeChecker in
   let module CU = CicUniv in
   (* no idea why ocaml wants this *)
-  let advance ?statement () = script#advance ?statement () in
   let parsed_text_length = String.length parsed_text in
-  let dbd = MatitaDb.instance () 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 l =  MQ.match_term ~dbd term in
-      let query_url =
-        MatitaMisc.strip_suffix ~suffix:"."
-          (HExtlib.trim_blanks unparsed_text)
-      in
-      let entry = `Whelp (query_url, l) in
-      guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
-      [], parsed_text_length
+     let l =  Whelp.match_term ~dbd term in
+     let query_url =
+       MatitaMisc.strip_suffix ~suffix:"."
+         (HExtlib.trim_blanks unparsed_text)
+     in
+     let entry = `Whelp (query_url, l) in
+     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 l = MQ.instance ~dbd term in
-      let entry = `Whelp (TAPp.pp_macro_cic (TA.WInstance (loc, term)), l) in
-      guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
-      [], parsed_text_length
+     let l = Whelp.instance ~dbd term 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 = MQ.locate ~dbd s in
-      let entry = `Whelp (TAPp.pp_macro_cic (TA.WLocate (loc, s)), l) in
-      guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
-      [], parsed_text_length
+     let l = Whelp.locate ~dbd s 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 uri =
-        match term with
-        | Cic.MutInd (uri,n,_) -> UriManager.uri_of_uriref uri n None 
-        | _ -> failwith "Not a MutInd"
-      in
-      let l = MQ.elim ~dbd uri in
-      let entry = `Whelp (TAPp.pp_macro_cic (TA.WElim (loc, term)), l) in
-      guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
-      [], parsed_text_length
+     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 (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 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
-      guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
-      [], parsed_text_length
+     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 (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 = MatitaTypes.get_current_proof status in
-      let proof_status = proof, user_goal in
+      let user_goal' =
+       match user_goal with
+          Some n -> n
+        | None -> raise NoUnfinishedProof
+      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
       (match selected with
       | [] -> [], parsed_text_length
       | [uri] -> 
           let suri = UriManager.string_of_uri uri in
-          let ast 
+          let ast loc =
             TA.Executable (loc, (TA.Tactical (loc,
               TA.Tactic (loc,
                 TA.Apply (loc, CicNotationPt.Uri (suri, None))),
-                Some (TA.Dot loc))))
+                Some (TA.Dot loc)))) in
+          let text =
+           comment parsed_text ^ "\n" ^
+            pp_eager_statement_ast (ast HExtlib.dummy_floc) in
+          let text_len = String.length text in
+          let loc = HExtlib.floc_of_loc (0,text_len) in
+          let statement = `Ast (GrafiteParser.LSome (ast loc),text) in
+          let res,_parsed_text_len =
+           eval_statement include_paths buffer guistuff lexicon_status
+            grafite_status user_goal script statement
           in
-        let new_status = MatitaEngine.eval_ast status ast in
-        let extra_text = 
-          comment parsed_text ^ 
-          "\n" ^ TAPp.pp_statement ast
-        in
-        [ new_status , (extra_text, ast) ], parsed_text_length
+           (* we need to replace all the parsed_text *)
+           res,String.length parsed_text
       | _ -> 
-          MatitaLog.error 
+          HLog.error 
             "The result of the urichooser should be only 1 uri, not:\n";
           List.iter (
-            fun u -> MatitaLog.error (UriManager.string_of_uri u ^ "\n")
+            fun u -> HLog.error (UriManager.string_of_uri u ^ "\n")
           ) 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 interps = 
-        MatitaDisambiguator.disambiguate_term ~dbd ~context ~metasenv
-         ~aliases:status.aliases ~universe:(Some status.multi_aliases) term
-      in
-      let _, metasenv , term, ugraph =
-        match interps with 
-        | [x], _ -> x
-        | _ -> assert false
-      in
-      let ty,_ = CTC.type_of_aux' metasenv context term ugraph in
+      let metasenv = GrafiteTypes.get_proof_metasenv grafite_status in
+      let context =
+       match user_goal with
+          None -> []
+        | Some n -> GrafiteTypes.get_proof_context grafite_status n in
+      let ty,_ = CTC.type_of_aux' metasenv context term CicUniv.empty_ugraph in
       let t_and_ty = Cic.Cast (term,ty) in
       guistuff.mathviewer#show_entry (`Cic (t_and_ty,metasenv));
       [], parsed_text_length
-(*   | TA.Abort _ -> 
-      let rec go_back () =
-        let status = script#status.proof_status in
-        match status with
-        | No_proof -> ()
-        | _ -> script#retract ();go_back()
-      in
-      [], parsed_text_length, Some go_back
-  | TA.Redo (_, Some i) ->  [], parsed_text_length, 
-      Some (fun () -> for j = 1 to i do advance () done)
-  | TA.Redo (_, None) ->   [], parsed_text_length, 
-      Some (fun () -> advance ())
-  | TA.Undo (_, Some i) ->  [], parsed_text_length, 
-      Some (fun () -> for j = 1 to i do script#retract () done)
-  | TA.Undo (_, None) -> [], parsed_text_length, 
-      Some (fun () -> script#retract ()) *)
   (* TODO *)
   | TA.Quit _ -> failwith "not implemented"
   | TA.Print (_,kind) -> failwith "not implemented"
   | 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
+and eval_executable include_paths (buffer : GText.buffer) guistuff lexicon_status grafite_status user_goal unparsed_text parsed_text script loc ex
 =
-  let module TAPp = GrafiteAstPp in
-  let module MD = MatitaDisambiguator in
-  let module ML = MatitacleanLib in
-  let parsed_text_length = String.length parsed_text in
-  match ex with
-  | TA.Command (loc, _) | TA.Tactical (loc, _, _) ->
-      (try 
-        (match MatitaMisc.baseuri_of_baseuri_decl (TA.Executable (loc,ex)) with
-        | None -> ()
-        | Some u -> 
-            if not (MatitaMisc.is_empty u) then
-              match 
-                guistuff.ask_confirmation 
-                  ~title:"Baseuri redefinition" 
-                  ~message:(
-                    "Baseuri " ^ u ^ " already exists.\n" ^
-                    "Do you want to redefine the corresponding "^
-                    "part of the library?")
-              with
-              | `YES -> MatitacleanLib.clean_baseuris [u]
-              | `NO -> ()
-              | `CANCEL -> raise MatitaTypes.Cancel);
-        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
-
-let rec eval_statement (buffer : GText.buffer) guistuff status user_goal
- script statement
+ let module TAPp = GrafiteAstPp in
+ let module MD = GrafiteDisambiguator in
+ let module ML = MatitaMisc in
+  try
+   begin
+    match ex with
+     | TA.Command (_,TA.Set (_,"baseuri",u)) ->
+        if not (GrafiteMisc.is_empty u) then
+         (match 
+            guistuff.ask_confirmation 
+              ~title:"Baseuri redefinition" 
+              ~message:(
+                "Baseuri " ^ u ^ " already exists.\n" ^
+                "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)
+     | _ -> ()
+   end;
+   eval_with_engine
+    guistuff lexicon_status grafite_status user_goal parsed_text
+     (TA.Executable (loc, ex))
+  with
+     MatitaTypes.Cancel -> [], 0
+   | GrafiteEngine.Macro (_loc,lazy_macro) ->
+      let context =
+       match user_goal with
+          None -> []
+        | Some n -> GrafiteTypes.get_proof_context grafite_status n in
+      let grafite_status,macro = lazy_macro context in
+       eval_macro include_paths buffer guistuff lexicon_status grafite_status
+        user_goal unparsed_text parsed_text script macro
+
+and eval_statement include_paths (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
+        let ast = 
+          wrap_with_developments guistuff
+            (GrafiteParser.parse_statement 
+              (Ulexing.from_utf8_string text) ~include_paths) lexicon_status 
+        in
+          ast, 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
@@ -388,33 +372,40 @@ 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],
+        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)
-       with HExtlib.Localized (floc, exn) ->
-        HExtlib.raise_localized_exception
-         ~offset:parsed_text_length floc exn
+        eval_statement include_paths 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
+        | GrafiteDisambiguator.DisambiguationError (offset,errorll) ->
+           raise
+            (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)::tl ->
+         (statuses,parsed_text ^ text)::tl,parsed_text_length + len
       | [] -> [], 0)
-  | 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 
+  | GrafiteParser.LSome (GrafiteAst.Executable (loc, ex)) ->
+     let parsed_text, parsed_text_length = text_of_loc loc in
+      eval_executable include_paths buffer guistuff lexicon_status
+       grafite_status user_goal unparsed_text parsed_text script loc ex
   
 let fresh_script_id =
   let i = ref 0 in
   fun () -> incr i; !i
 
 class script  ~(source_view: GSourceView.source_view)
-              ~(init: MatitaTypes.status) 
               ~(mathviewer: MatitaTypes.mathViewer) 
               ~set_star
               ~ask_confirmation
@@ -423,7 +414,20 @@ class script  ~(source_view: GSourceView.source_view)
               () =
 let buffer = source_view#buffer in
 let source_buffer = source_view#source_buffer in
+let initial_statuses =
+ (* these include_paths are used only to load the initial notation *)
+ 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 mutable include_paths =
+   Helm_registry.get_list Helm_registry.string "matita.includes"
+
   val scriptId = fresh_script_id ()
   
   val guistuff = {
@@ -449,15 +453,16 @@ 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.
       * Invariant: this list length is 1 + length of statements *)
 
   (** goal as seen by the user (i.e. metano corresponding to current tab) *)
-  val mutable userGoal = ~-1
+  val mutable userGoal = None
 
   (** text mark and tag representing locked part of a script *)
   val locked_mark =
@@ -470,59 +475,53 @@ 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
-      in
-      let (new_statuses, new_statements, new_asts) =
-        let statuses, statements = List.split entries in
-        let texts, asts = List.split statements in
-        statuses, texts, asts
-      in
-      history <- List.rev new_statuses @ history;
-      statements <- List.rev new_statements @ statements;
-      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
-        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;
-          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 -> ())
-      | _ -> ())
-      *)
-    in
-    let s = match statement with Some s -> s | None -> self#getFuture in
-    MatitaLog.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;
+   let s = match statement with Some s -> s | None -> self#getFuture in
+   HLog.debug ("evaluating: " ^ first_line s ^ " ...");
+   let (entries, parsed_len) = 
+    try
+     eval_statement include_paths buffer guistuff self#lexicon_status
+      self#grafite_status userGoal self (`Raw s)
+    with End_of_file -> raise Margin
+   in
+   let new_statuses, new_statements =
+     let statuses, texts = List.split entries in
+     statuses, texts
+   in
+   history <- new_statuses @ history;
+   statements <- new_statements @ statements;
+   let start = buffer#get_iter_at_mark (`MARK locked_mark) in
+   let new_text = String.concat "" (List.rev new_statements) in
+   if statement <> None then
+     buffer#insert ~iter:start new_text
+   else begin
+     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;
+   end;
+   self#moveMark (String.length new_text);
+   (* here we need to set the Goal in case we are going to cursor (or to
+      bottom) and we will face a macro *)
+   match self#grafite_status.proof_status with
+      Incomplete_proof p ->
+       userGoal <-
+         (try Some (Continuationals.Stack.find_goal p.stack)
+         with Failure _ -> None)
+    | _ -> userGoal <- None
+
+  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)
@@ -537,14 +536,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
@@ -585,12 +585,13 @@ object (self)
 
   val mutable observers = []
 
-  method addObserver (o: MatitaTypes.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);
@@ -599,8 +600,17 @@ object (self)
     
   method assignFileName file =
     let abspath = MatitaMisc.absolute_path file in
-    let devel = MatitamakeLib.development_for_dir (Filename.dirname abspath) in
-    guistuff.filenamedata <- Some abspath, devel
+    let dirname = Filename.dirname abspath in
+    let devel = MatitamakeLib.development_for_dir dirname in
+    guistuff.filenamedata <- Some abspath, devel;
+    let include_ = 
+     match MatitamakeLib.development_for_dir dirname with
+        None -> []
+      | Some devel -> [MatitamakeLib.root_for_development devel] in
+    let include_ =
+     include_ @ (Helm_registry.get_list Helm_registry.string "matita.includes")
+    in
+     include_paths <- include_
     
   method saveToFile () =
     let oc = open_out self#getFilename in
@@ -617,16 +627,26 @@ object (self)
         output_string oc (buffer#get_text ~start:buffer#start_iter
                             ~stop:buffer#end_iter ());
         close_out oc;
-        MatitaLog.debug ("backup " ^ f ^ " saved")                    
+        HLog.debug ("backup " ^ f ^ " saved")                    
       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 ];
-    userGoal <- ~-1;
+    history <- [ initial_statuses ];
+    userGoal <- None;
     self#notify;
     buffer#remove_tag locked_tag ~start:buffer#start_iter ~stop:buffer#end_iter;
     buffer#move_mark (`MARK locked_mark) ~where:buffer#start_iter
@@ -636,15 +656,24 @@ 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 
     buffer#insert ~iter:(buffer#get_iter `START) template;
-    guistuff.filenamedata <- 
-      (None,MatitamakeLib.development_for_dir (Unix.getcwd ()));
-    buffer#set_modified false;
-    set_star (Filename.basename self#ppFilename) false
+    let development = MatitamakeLib.development_for_dir (Unix.getcwd ()) in
+    guistuff.filenamedata <- (None,development);
+    let include_ = 
+     match development with
+        None -> []
+      | Some devel -> [MatitamakeLib.root_for_development devel ]
+    in
+    let include_ =
+     include_ @ (Helm_registry.get_list Helm_registry.string "matita.includes")
+    in
+     include_paths <- include_ ;
+     buffer#set_modified false;
+     set_star (Filename.basename self#ppFilename) false
 
   method goto (pos: [`Top | `Bottom | `Cursor]) () =
     let old_locked_mark =
@@ -703,8 +732,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
@@ -726,45 +757,59 @@ 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 = 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#grafite_status
+
+  method proofContext =
+   match userGoal with
+      None -> []
+    | Some n -> GrafiteTypes.get_proof_context self#grafite_status n
+
+  method proofConclusion =
+   match userGoal with
+      None -> assert false
+    | Some n ->
+       GrafiteTypes.get_proof_conclusion self#grafite_status n
+
+  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_only_comments 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 lexicon_status
+      in
       match st with
-      | GrafiteAst.Comment (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_only_comments lexicon_status next
+      | GrafiteParser.LNone _
+      | GrafiteParser.LSome (GrafiteAst.Executable _) -> false
     in
     try
-      is_there_and_executable s
+      is_there_only_comments self#lexicon_status s
     with 
     | CicNotationParser.Parse_error _ -> false
     | Margin | End_of_file -> true
 
   (* debug *)
   method dump () =
-    MatitaLog.debug "script status:";
-    MatitaLog.debug ("history size: " ^ string_of_int (List.length history));
-    MatitaLog.debug (sprintf "%d statements:" (List.length statements));
-    List.iter MatitaLog.debug statements;
-    MatitaLog.debug ("Current file name: " ^
+    HLog.debug "script status:";
+    HLog.debug ("history size: " ^ string_of_int (List.length history));
+    HLog.debug (sprintf "%d statements:" (List.length statements));
+    List.iter HLog.debug statements;
+    HLog.debug ("Current file name: " ^
       (match guistuff.filenamedata with 
       |None,_ -> "[ no name ]" 
       | Some f,_ -> f));
@@ -773,10 +818,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