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);
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 =
+ try
+ Librarian.baseuri_of_script ~include_paths mafilename
+ with Librarian.NoRootFor _ -> raise exn
+ in
+ if MatitacLib.Make.make root [tgt] then f x
+ else raise (Failure ("Compiling: " ^ tgt))
;;
-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
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
| `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
~set_star
~ask_confirmation
~urichooser
- ~rootcreator
() =
let buffer = source_view#buffer in
let source_buffer = source_view#source_buffer in
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 ()
method has_name = filename_ <> None
- method buri_of_current_file =
+ method include_paths =
+ include_paths_ @
+ Helm_registry.get_list Helm_registry.string "matita.includes"
+
+ 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 f in buri
+ try
+ let _root, buri, _fname, _tgt =
+ Librarian.baseuri_of_script ~include_paths:self#include_paths f
+ in
+ buri
with Librarian.NoRootFor _ -> default_buri
method filename = match filename_ with None -> default_fname | Some f -> f
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
- 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
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
+ 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
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,_)) ->
HLog.debug (sprintf "%d statements:" (List.length statements));
List.iter HLog.debug statements;
HLog.debug ("Current file name: " ^ self#filename);
- HLog.debug ("Current buri: " ^ self#buri_of_current_file);
end
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