mathviewer:MatitaTypes.mathViewer;
urichooser: UriManager.uri list -> UriManager.uri list;
ask_confirmation: title:string -> message:string -> [`YES | `NO | `CANCEL];
- develcreator: containing:string option -> unit;
}
-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
([],skipped_txt) enriched_history_fragment
in
res,"",parsed_text_length
+;;
-let wrap_with_developments guistuff f arg =
- let compile_needed_and_go_on lexiconfile d exc =
- let target = Pcre.replace ~pat:"lexicon$" ~templ:"moo" lexiconfile in
- let target = Pcre.replace ~pat:"metadata$" ~templ:"moo" target 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
- f arg
- in
- let do_nothing () = raise (ActionCancelled "Inclusion not performed") in
- let check_if_file_is_exists f =
- assert(Pcre.pmatch ~pat:"ma$" f);
- let pwd = Sys.getcwd () in
- let f_pwd = pwd ^ "/" ^ f in
- if not (HExtlib.is_regular f_pwd) then
- raise (ActionCancelled ("File "^f_pwd^" does not exists!"))
- else
- raise
- (ActionCancelled
- ("Internal error: "^f_pwd^" exists but I'm unable to include it!"))
- in
- let handle_with_devel d lexiconfile mafile exc =
- let name = MatitamakeLib.name_for_development d in
- let title = "Unable to include " ^ lexiconfile in
- let message =
- mafile ^ " is handled by development <b>" ^ name ^ "</b>.\n\n" ^
- "<i>Should I compile it and Its dependencies?</i>"
- in
- (match guistuff.ask_confirmation ~title ~message with
- | `YES -> compile_needed_and_go_on lexiconfile d exc
- | `NO -> raise exc
- | `CANCEL -> do_nothing ())
- in
- let handle_without_devel mafilename exc =
- let title = "Unable to include " ^ mafilename in
- let message =
- mafilename ^ " is <b>not</b> handled by a development.\n" ^
- "All dependencies are automatically solved for a development.\n\n" ^
- "<i>Do you want to set up a development?</i>"
- in
- (match guistuff.ask_confirmation ~title ~message with
- | `YES ->
- guistuff.develcreator ~containing:(Some (Filename.dirname mafilename));
- do_nothing ()
- | `NO -> raise exc
- | `CANCEL -> do_nothing())
- in
- try
- f arg
+(* 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 ~never_include:true ~include_paths 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);
- 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' *)
- match MatitamakeLib.development_for_dir (Filename.dirname mafilename) with
- | None -> handle_without_devel mafilename exn
- | Some d -> handle_with_devel d xfilename mafilename exn
-;;
-
-let eval_with_engine
- guistuff lexicon_status grafite_status user_goal
- skipped_txt nonskipped_txt st
-=
- wrap_with_developments guistuff
- (eval_with_engine
- guistuff lexicon_status grafite_status user_goal
- skipped_txt nonskipped_txt) st
+ | GrafiteParser.NoInclusionPerformed mafilename ->
+ let root, buri, _, tgt =
+ 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
+ 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))) ;
- 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_developments 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
- ~develcreator
() =
let buffer = source_view#buffer in
let source_buffer = source_view#source_buffer in
let initial_statuses baseuri =
- (* 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
+ CicNotation2.load_notation ~include_paths:[]
+ BuildTimeConf.core_notation_script
+ 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 =
- Helm_registry.get_list Helm_registry.string "matita.includes"
+ val mutable include_paths_ = []
val scriptId = fresh_script_id ()
-
+
val guistuff = {
mathviewer = mathviewer;
urichooser = urichooser;
ask_confirmation = ask_confirmation;
- develcreator=develcreator;}
+ }
+
+ val mutable filename_ = (None : string option)
+
+ method has_name = filename_ <> None
+
+ 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 ~include_paths:self#include_paths f
+ in
+ buri
+ with Librarian.NoRootFor _ -> default_buri
+
+ method filename = match filename_ with None -> default_fname | Some f -> f
initializer
ignore (GMain.Timeout.add ~ms:300000
~callback:(fun _ -> self#_saveToBackupFile ();true));
ignore (buffer#connect#modified_changed
- (fun _ -> set_star (Filename.basename (Librarian.filename ())) buffer#modified))
+ (fun _ -> set_star buffer#modified))
val mutable statements = [] (** executed statements *)
- val mutable history = [ initial_statuses "cic:/matita/test/" ]
+ val mutable history = [ initial_statuses default_buri ]
(** 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.
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 root, buri, file = Librarian.baseuri_of_script ~include_paths file in
- Helm_registry.set "matita.filename" file;
- self#reset_buffer
+ let file =
+ match file with
+ | Some f -> Some (Librarian.absolutize f)
+ | None -> None
+ in
+ self#goto_top;
+ filename_ <- file;
+ 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 () =
- let oc = open_out (Librarian.filename ()) in
- output_string oc (buffer#get_text ~start:buffer#start_iter
+ 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 ());
- close_out oc;
- buffer#set_modified false
+ close_out oc;
+ set_star false;
+ buffer#set_modified false
+ else
+ HLog.error "Can't save, no filename selected"
method private _saveToBackupFile () =
if buffer#modified then
begin
- let f = Librarian.filename () ^ "~" in
+ let f = self#filename in
let oc = open_out f in
output_string oc (buffer#get_text ~start:buffer#start_iter
~stop:buffer#end_iter ());
LexiconSync.time_travel ~present:self#lexicon_status ~past:lexicon_status
method private reset_buffer =
- let file = Librarian.filename () in
- let root, buri, file = Librarian.baseuri_of_script file in
statements <- [];
- history <- [ initial_statuses buri ];
+ history <- [ initial_statuses self#buri_of_current_file ];
userGoal <- None;
self#notify;
buffer#remove_tag locked_tag ~start:buffer#start_iter ~stop:buffer#end_iter;
let template = HExtlib.input_file BuildTimeConf.script_template in
buffer#insert ~iter:(buffer#get_iter `START) template;
buffer#set_modified false;
- set_star (Filename.basename (Librarian.filename ())) false
+ set_star false
method goto (pos: [`Top | `Bottom | `Cursor]) () =
try
method setGoal n = userGoal <- n
method goal = userGoal
+ method bos =
+ match history with
+ | _::[] -> true
+ | _ -> false
+
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 lexicon_status
+ ~include_paths:self#include_paths lexicon_status
in
match st with
| GrafiteParser.LSome (GrafiteAst.Comment (loc,_)) ->
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: " ^ Librarian.filename ());
+ HLog.debug ("Current file name: " ^ self#filename);
end
let _script = ref None
-let script ~source_view ~mathviewer ~urichooser ~develcreator ~ask_confirmation ~set_star ()
+let script ~source_view ~mathviewer ~urichooser ~ask_confirmation ~set_star ()
=
let s = new script
- ~source_view ~mathviewer ~ask_confirmation ~urichooser ~develcreator ~set_star ()
+ ~source_view ~mathviewer ~ask_confirmation ~urichooser ~set_star ()
in
_script := Some s;
s
projects / helm.git / blobdiff