From b36918dbc0e6d0c70c92551e34bdc65cbfddddec Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 6 Jan 2008 22:35:53 +0000 Subject: [PATCH] matita now includes compiling. if the file is not compiled it compiles it, but if it is compiled it does not check that it may need to be rebuilt --- components/library/librarian.mli | 4 +- matita/matitaGui.ml | 2 + matita/matitaScript.ml | 66 +++++++++++++++++++++++--------- matita/matitaScript.mli | 1 + 4 files changed, 54 insertions(+), 19 deletions(-) diff --git a/components/library/librarian.mli b/components/library/librarian.mli index 839d8daa1..1c305c265 100644 --- a/components/library/librarian.mli +++ b/components/library/librarian.mli @@ -2,7 +2,9 @@ exception NoRootFor of string val find_root: string -> string -(* val parse_root: string -> (string*string) list *) +val load_root_file: string -> (string*string) list + +val absolutize: string -> string (* baseuri_of_script ?(inc:REG[matita.includes]) fname * -> diff --git a/matita/matitaGui.ml b/matita/matitaGui.ml index 7fe9cdedb..b2f509b25 100644 --- a/matita/matitaGui.ml +++ b/matita/matitaGui.ml @@ -58,6 +58,7 @@ class console ~(buffer: GText.buffer) () = method clear () = buffer#delete ~start:buffer#start_iter ~stop:buffer#end_iter method log_callback (tag: HLog.log_tag) s = + let s = Pcre.replace ~pat:"\\[0;3.m([^]+)\\[0m" ~templ:"$1" s in match tag with | `Debug -> self#debug (s ^ "\n") | `Error -> self#error (s ^ "\n") @@ -1155,6 +1156,7 @@ class gui () = else begin script#assignFileName (Some file); + let file = script#filename in let content = if Sys.file_exists file then file else BuildTimeConf.script_template diff --git a/matita/matitaScript.ml b/matita/matitaScript.ml index 9dc930f18..fbe8730c4 100644 --- a/matita/matitaScript.ml +++ b/matita/matitaScript.ml @@ -102,15 +102,10 @@ let eval_with_engine guistuff lexicon_status grafite_status user_goal res,"",parsed_text_length ;; -let wrap_with_make g f x = +let wrap_with_make include_paths g f x = try f x with -(* - | DependenciesParser.UnableToInclude mafilename -> - assert (Pcre.pmatch ~pat:"ma$" mafilename); - check_if_file_is_exists mafilename -*) | LexiconEngine.IncludedFileNotCompiled (xfilename,mafilename) | GrafiteEngine.IncludedFileNotCompiled (xfilename,mafilename) as exn -> assert (Pcre.pmatch ~pat:"ma$" mafilename); @@ -118,14 +113,17 @@ let wrap_with_make g f x = 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' *) - raise exn + let root, buri, _, tgt = + Librarian.baseuri_of_script ~include_paths mafilename + in + if MatitacLib.Make.make root [tgt] then f x else raise exn ;; -let eval_with_engine +let eval_with_engine include_paths guistuff lexicon_status grafite_status user_goal skipped_txt nonskipped_txt st = - wrap_with_make guistuff + wrap_with_make include_paths guistuff (eval_with_engine guistuff lexicon_status grafite_status user_goal skipped_txt nonskipped_txt) st @@ -609,7 +607,7 @@ script ex loc ignore (buffer#move_mark (`NAME "beginning_of_statement") ~where:((buffer#get_iter_at_mark (`NAME "locked"))#forward_chars (Glib.Utf8.length skipped_txt))) ; - eval_with_engine + eval_with_engine include_paths guistuff lexicon_status grafite_status user_goal skipped_txt nonskipped_txt (TA.Executable (loc, ex)) with @@ -631,7 +629,7 @@ and eval_statement include_paths (buffer : GText.buffer) guistuff lexicon_status | `Raw text -> if Pcre.pmatch ~rex:only_dust_RE text then raise Margin; let ast = - wrap_with_make guistuff + wrap_with_make include_paths guistuff (GrafiteParser.parse_statement (Ulexing.from_utf8_string text) ~include_paths) lexicon_status in @@ -702,11 +700,22 @@ let initial_statuses baseuri = let grafite_status = GrafiteSync.init baseuri in grafite_status,lexicon_status in +let read_include_paths file = + try + let root, _buri, _fname, _tgt = + Librarian.baseuri_of_script ~include_paths:[] file + in + let rc = + Str.split (Str.regexp " ") + (List.assoc "include_paths" (Librarian.load_root_file (root^"/root"))) + in + List.iter (HLog.debug) rc; rc + with Librarian.NoRootFor _ | Not_found -> [] +in let default_buri = "cic:/matita/tests" in let default_fname = ".unnamed.ma" in object (self) - val mutable include_paths = (* FIXME, reset every time a new root is entered *) - Helm_registry.get_list Helm_registry.string "matita.includes" + val mutable include_paths_ = [] val scriptId = fresh_script_id () @@ -720,13 +729,25 @@ object (self) method has_name = filename_ <> None + method include_paths = + include_paths_ + + method private curdir = + try + let root, _buri, _fname, _tgt = + Librarian.baseuri_of_script ~include_paths:self#include_paths + self#filename + in + root + with Librarian.NoRootFor _ -> Sys.getcwd () + method buri_of_current_file = match filename_ with | None -> default_buri | Some f -> try let _root, buri, _fname, _tgt = - Librarian.baseuri_of_script ~include_paths f + Librarian.baseuri_of_script ~include_paths:self#include_paths f in buri with Librarian.NoRootFor _ -> default_buri @@ -773,7 +794,7 @@ object (self) HLog.debug ("evaluating: " ^ first_line s ^ " ..."); let entries, newtext, parsed_len = try - eval_statement include_paths buffer guistuff self#lexicon_status + eval_statement self#include_paths buffer guistuff self#lexicon_status self#grafite_status userGoal self (`Raw s) with End_of_file -> raise Margin in @@ -898,11 +919,20 @@ object (self) buffer#set_text (HExtlib.input_file f); self#reset_buffer; buffer#set_modified false - + method assignFileName file = + let file = + match file with + | Some f -> Some (Librarian.absolutize f) + | None -> None + in self#goto_top; filename_ <- file; - self#reset_buffer + include_paths_ <- + (match file with Some file -> read_include_paths file | None -> []); + self#reset_buffer; + Sys.chdir self#curdir; + HLog.debug ("Moving to " ^ Sys.getcwd ()) method saveToFile () = if self#has_name && buffer#modified then @@ -1079,7 +1109,7 @@ object (self) 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 lexicon_status + ~include_paths:self#include_paths lexicon_status in match st with | GrafiteParser.LSome (GrafiteAst.Comment (loc,_)) -> diff --git a/matita/matitaScript.mli b/matita/matitaScript.mli index e8b80d25b..d4c82321e 100644 --- a/matita/matitaScript.mli +++ b/matita/matitaScript.mli @@ -56,6 +56,7 @@ object (* alwais return a name, use has_name to check if it is the default one *) method filename: string method buri_of_current_file: string + method include_paths: string list method assignFileName : string option -> unit (* to the current active file *) method loadFromFile : string -> unit method loadFromString : string -> unit -- 2.39.2