type guistuff = {
mathviewer:MatitaTypes.mathViewer;
- urichooser: UriManager.uri list -> UriManager.uri list;
+ urichooser: NReference.reference list -> NReference.reference list;
ask_confirmation: title:string -> message:string -> [`YES | `NO | `CANCEL];
}
let text = skipped_txt ^ nonskipped_txt in
let prefix_len = MatitaGtkMisc.utf8_string_length skipped_txt in
let enriched_history_fragment =
- MatitaEngine.eval_ast ~do_heavy_checks:(Helm_registry.get_bool
+ MatitaEngine.eval_ast ~include_paths ~do_heavy_checks:(Helm_registry.get_bool
"matita.do_heavy_checks")
grafite_status (text,prefix_len,st)
in
match alias with
| None -> (status,to_prepend ^ nonskipped_txt)::acc,""
| Some (k,value) ->
- let newtxt = LexiconAstPp.pp_alias value in
+ let newtxt = GrafiteAstPp.pp_alias value in
(status,to_prepend ^ newtxt ^ "\n")::acc, "")
([],skipped_txt) enriched_history_fragment
in
* so that we can ensure the inclusion is performed after the included file
* is compiled (if needed). matitac does not need that, since it compiles files
* in the good order, here files may be compiled on demand. *)
-let wrap_with_make include_paths (f : #LexiconEngine.status GrafiteParser.statement) x =
- try
- f ~never_include:true ~include_paths x
- with
- | GrafiteParser.NoInclusionPerformed mafilename ->
+let wrap_with_make include_paths f x =
+ match f x with
+ GrafiteParser.LSome (GrafiteAst.Executable (_,GrafiteAst.NCommand
+ (_,GrafiteAst.Include (_,_,mafilename)))) as cmd ->
let root, buri, _, tgt =
try Librarian.baseuri_of_script ~include_paths mafilename
with Librarian.NoRootFor _ ->
HLog.error "please create it.";
raise (Failure ("No root file for "^mafilename))
in
- let b = MatitacLib.Make.make root [tgt] in
- if b then
- try f ~include_paths x with LexiconEngine.IncludedFileNotCompiled _ ->
- raise
- (Failure ("Including: "^tgt^
- "\nNothing to do... did you run matitadep?"))
+ if MatitacLib.Make.make root [tgt] then
+ cmd
else raise (Failure ("Compiling: " ^ tgt))
+ | cmd -> cmd
;;
-let pp_eager_statement_ast =
- GrafiteAstPp.pp_statement ~term_pp:NotationPp.pp_term
- ~lazy_term_pp:(fun _ -> assert false) ~obj_pp:(fun _ -> assert false)
+let pp_eager_statement_ast = GrafiteAstPp.pp_statement
let eval_nmacro include_paths (buffer : GText.buffer) guistuff grafite_status user_goal unparsed_text parsed_text script mac =
let parsed_text_length = String.length parsed_text in
in
let m, s, status, t =
GrafiteDisambiguate.disambiguate_nterm
- None status ctx menv subst (parsed_text,parsed_text_length,
+ status None ctx menv subst (parsed_text,parsed_text_length,
NotationPt.Cast (t,NotationPt.Implicit `JustOne))
(* XXX use the metasenv, if possible *)
in
and eval_statement include_paths (buffer : GText.buffer) guistuff
grafite_status user_goal script statement
=
- let (grafite_status,st), unparsed_text =
+ let st,unparsed_text =
match statement with
| `Raw text ->
if Pcre.pmatch ~rex:only_dust_RE text then raise Margin;
let ast =
wrap_with_make include_paths
- (GrafiteParser.parse_statement (Ulexing.from_utf8_string text))
- grafite_status
+ (GrafiteParser.parse_statement grafite_status)
+ (Ulexing.from_utf8_string text)
in
ast, text
- | `Ast (st, text) -> (grafite_status, st), text
+ | `Ast (st, text) -> st, text
in
let text_of_loc floc =
let nonskipped_txt,_ = MatitaGtkMisc.utf8_parsed_text unparsed_text floc in
let buffer = source_view#buffer in
let source_buffer = source_view#source_buffer in
let initial_statuses current baseuri =
- let empty_lstatus = new LexiconEngine.status in
+ let empty_lstatus = new GrafiteDisambiguate.status in
(match current with
Some current ->
- LexiconSync.time_travel ~present:current ~past:empty_lstatus;
- GrafiteSync.time_travel ~present:current ();
+ NCicLibrary.time_travel
+ ((new GrafiteTypes.status current#baseuri)#set_disambiguate_db current#disambiguate_db);
(* CSC: there is a known bug in invalidation; temporary fix here *)
NCicEnvironment.invalidate ()
| None -> ());
- let lexicon_status =
- CicNotation2.load_notation ~include_paths:[] empty_lstatus
- BuildTimeConf.core_notation_script
- in
- let grafite_status = GrafiteSync.init lexicon_status baseuri in
+ let lexicon_status = empty_lstatus in
+ let grafite_status = (new GrafiteTypes.status baseuri)#set_disambiguate_db lexicon_status#disambiguate_db in
grafite_status
in
let read_include_paths file =
bottom) and we will face a macro *)
userGoal <- None
- method private _retract offset grafite_status new_statements
- new_history
- =
- let cur_grafite_status =
- match history with s::_ -> s | [] -> assert false
- in
- LexiconSync.time_travel ~present:cur_grafite_status ~past:grafite_status;
- GrafiteSync.time_travel ~present:cur_grafite_status ~past:grafite_status ();
+ method private _retract offset grafite_status new_statements new_history =
+ NCicLibrary.time_travel grafite_status;
statements <- new_statements;
history <- new_history;
self#moveMark (- offset)
method eos =
let rec is_there_only_comments lexicon_status s =
if Pcre.pmatch ~rex:only_dust_RE s then raise Margin;
- let lexicon_status,st =
- GrafiteParser.parse_statement (Ulexing.from_utf8_string s)
- ~include_paths:self#include_paths lexicon_status
- in
- match st with
+ match
+ GrafiteParser.parse_statement lexicon_status (Ulexing.from_utf8_string s)
+ with
| GrafiteParser.LSome (GrafiteAst.Comment (loc,_)) ->
let _,parsed_text_length = MatitaGtkMisc.utf8_parsed_text s loc in
(* CSC: why +1 in the following lines ???? *)
in
try is_there_only_comments self#grafite_status self#getFuture
with
- | LexiconEngine.IncludedFileNotCompiled _
+ | NCicLibrary.IncludedFileNotCompiled _
| HExtlib.Localized _
| CicNotationParser.Parse_error _ -> false
| Margin | End_of_file -> true
projects / helm.git / blobdiff