ask_confirmation: title:string -> message:string -> [`YES | `NO | `CANCEL];
}
-let eval_with_engine guistuff lexicon_status grafite_status user_goal
+let eval_with_engine include_paths guistuff lexicon_status grafite_status user_goal
skipped_txt nonskipped_txt st
=
let module TAPp = GrafiteAstPp in
res,"",parsed_text_length
;;
-let wrap_with_make include_paths g f x =
+(* this function calls the parser in a way that it does not perform inclusions,
+ * 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 : GrafiteParser.statement) x =
try
- f x
+ f ~never_include:true ~include_paths x
with
- | LexiconEngine.IncludedFileNotCompiled (xfilename,mafilename)
- | GrafiteEngine.IncludedFileNotCompiled (xfilename,mafilename) as exn ->
- assert (Pcre.pmatch ~pat:"ma$" mafilename);
- assert (Pcre.pmatch ~pat:"lexicon$" xfilename ||
- Pcre.pmatch ~pat:"mo$" xfilename );
- (* we know that someone was able to include the .ma, get the baseuri
- * but was unable to get the compilation output 'xfilename' *)
+ | GrafiteParser.NoInclusionPerformed mafilename ->
let root, buri, _, tgt =
- Librarian.baseuri_of_script ~include_paths mafilename
+ try Librarian.baseuri_of_script ~include_paths mafilename
+ with Librarian.NoRootFor _ ->
+ HLog.error ("The included file '"^mafilename^"' has no root file,");
+ HLog.error "please create it.";
+ raise (Failure ("No root file for "^mafilename))
in
- if MatitacLib.Make.make root [tgt] then f x else raise exn
-;;
-
-let eval_with_engine include_paths
- guistuff lexicon_status grafite_status user_goal
- skipped_txt nonskipped_txt st
-=
- wrap_with_make include_paths guistuff
- (eval_with_engine
- guistuff lexicon_status grafite_status user_goal
- skipped_txt nonskipped_txt) st
+ let initial_lexicon_status =
+ CicNotation2.load_notation ~include_paths:[] BuildTimeConf.core_notation_script
+ in
+ let b,x =
+ try
+ GrafiteSync.push ();
+ LexiconSync.time_travel ~present:x ~past:initial_lexicon_status;
+ let rc = MatitacLib.Make.make root [tgt] in
+ GrafiteSync.pop ();
+ CicNotation.reset ();
+ ignore(CicNotation2.load_notation ~include_paths:[]
+ BuildTimeConf.core_notation_script);
+ let x = List.fold_left (fun s c -> LexiconEngine.eval_command s c)
+ initial_lexicon_status (List.rev
+ x.LexiconEngine.lexicon_content_rev)
+ in
+ rc,x
+ with
+ | exn ->
+ HLog.error ("Unexpected " ^ snd(MatitaExcPp.to_string exn));
+ assert false
+ in
+ if b then f ~include_paths x
+ else raise (Failure ("Compiling: " ^ tgt))
;;
let pp_eager_statement_ast =
let module MD = GrafiteDisambiguator in
let module ML = MatitaMisc in
try
- begin
- match ex with
- | TA.Command (_,TA.Set (_,"baseuri",u)) ->
- if Http_getter_storage.is_read_only u then
- raise (ActionCancelled ("baseuri " ^ u ^ " is readonly"));
- if not (Http_getter_storage.is_empty ~local:true 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 -> LibraryClean.clean_baseuris [u]
- | `NO -> ()
- | `CANCEL -> raise MatitaTypes.Cancel)
- | _ -> ()
- end;
ignore (buffer#move_mark (`NAME "beginning_of_statement")
~where:((buffer#get_iter_at_mark (`NAME "locked"))#forward_chars
(Glib.Utf8.length skipped_txt))) ;
| `Raw text ->
if Pcre.pmatch ~rex:only_dust_RE text then raise Margin;
let ast =
- wrap_with_make include_paths guistuff
- (GrafiteParser.parse_statement
- (Ulexing.from_utf8_string text) ~include_paths) lexicon_status
+ wrap_with_make include_paths
+ (GrafiteParser.parse_statement (Ulexing.from_utf8_string text)) lexicon_status
in
ast, text
| `Ast (st, text) -> (lexicon_status, st), text
~set_star
~ask_confirmation
~urichooser
- ~rootcreator
() =
let buffer = source_view#buffer in
let source_buffer = source_view#source_buffer in
method has_name = filename_ <> None
method include_paths =
- include_paths_
+ include_paths_ @
+ Helm_registry.get_list Helm_registry.string "matita.includes"
method private curdir =
try
method private _advance ?statement () =
let s = match statement with Some s -> s | None -> self#getFuture in
+ if self#bos then LibraryClean.clean_baseuris [self#buri_of_current_file];
HLog.debug ("evaluating: " ^ first_line s ^ " ...");
let entries, newtext, parsed_len =
try
HLog.debug ("Moving to " ^ Sys.getcwd ())
method saveToFile () =
- if self#has_name && buffer#modified then
+ if self#has_name then
let oc = open_out self#filename in
output_string oc (buffer#get_text ~start:buffer#start_iter
~stop:buffer#end_iter ());
set_star false;
buffer#set_modified false
else
- if self#has_name then HLog.debug "No need to save"
- else HLog.error "Can't save, no filename selected"
+ HLog.error "Can't save, no filename selected"
method private _saveToBackupFile () =
if buffer#modified then
let _script = ref None
-let script ~source_view ~mathviewer ~urichooser ~rootcreator ~ask_confirmation ~set_star ()
+let script ~source_view ~mathviewer ~urichooser ~ask_confirmation ~set_star ()
=
let s = new script
- ~source_view ~mathviewer ~ask_confirmation ~urichooser ~rootcreator ~set_star ()
+ ~source_view ~mathviewer ~ask_confirmation ~urichooser ~set_star ()
in
_script := Some s;
s
projects / helm.git / blobdiff