let parsed_text_length = String.length parsed_text in
match mac with
| TA.Screenshot (_,name) ->
let parsed_text_length = String.length parsed_text in
match mac with
| TA.Screenshot (_,name) ->
| TA.NAutoInteractive (_, (Some _,_)) -> assert false
let rec eval_executable include_paths (buffer : GText.buffer) guistuff
| TA.NAutoInteractive (_, (Some _,_)) -> assert false
let rec eval_executable include_paths (buffer : GText.buffer) guistuff
=
try
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 include_paths
=
try
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 include_paths
(TA.Executable (loc, ex))
with
MatitaTypes.Cancel -> [], "", 0
| GrafiteEngine.NMacro (_loc,macro) ->
eval_nmacro include_paths buffer guistuff grafite_status
(TA.Executable (loc, ex))
with
MatitaTypes.Cancel -> [], "", 0
| GrafiteEngine.NMacro (_loc,macro) ->
eval_nmacro include_paths buffer guistuff grafite_status
| GrafiteAst.Executable (loc, ex) ->
let _, nonskipped, skipped, parsed_text_length = text_of_loc loc in
eval_executable include_paths buffer guistuff
| GrafiteAst.Executable (loc, ex) ->
let _, nonskipped, skipped, parsed_text_length = text_of_loc loc in
eval_executable include_paths buffer guistuff
| GrafiteAst.Comment (loc, GrafiteAst.Code (_, ex))
when Helm_registry.get_bool "matita.execcomments" ->
let _, nonskipped, skipped, parsed_text_length = text_of_loc loc in
eval_executable include_paths buffer guistuff
| GrafiteAst.Comment (loc, GrafiteAst.Code (_, ex))
when Helm_registry.get_bool "matita.execcomments" ->
let _, nonskipped, skipped, parsed_text_length = text_of_loc loc in
eval_executable include_paths buffer guistuff
| GrafiteAst.Comment (loc, _) ->
let parsed_text, _, _, parsed_text_length = text_of_loc loc in
let remain_len = String.length unparsed_text - parsed_text_length in
| GrafiteAst.Comment (loc, _) ->
let parsed_text, _, _, parsed_text_length = text_of_loc loc in
let remain_len = String.length unparsed_text - parsed_text_length in
with
HExtlib.Localized (floc, exn) ->
HExtlib.raise_localized_exception
with
HExtlib.Localized (floc, exn) ->
HExtlib.raise_localized_exception
let read_include_paths file =
try
let root, _buri, _fname, _tgt =
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")))
+ Librarian.baseuri_of_script ~include_paths:[] file in
+ let includes =
+ try
+ Str.split (Str.regexp " ")
+ (List.assoc "include_paths" (Librarian.load_root_file (root^"/root")))
+ with Not_found -> []
- List.iter (HLog.debug) rc; rc
- with Librarian.NoRootFor _ | Not_found -> []
+ let rc = root :: includes in
+ List.iter (HLog.debug) rc; rc
+ with Librarian.NoRootFor _ | Librarian.FileNotFound _ ->
+ []
method private curdir =
try
let root, _buri, _fname, _tgt =
method private curdir =
try
let root, _buri, _fname, _tgt =
MatitaMisc.observe_font_size (fun font_size ->
source_view#misc#modify_font_by_name
(sprintf "%s %d" BuildTimeConf.script_font font_size));
MatitaMisc.observe_font_size (fun font_size ->
source_view#misc#modify_font_by_name
(sprintf "%s %d" BuildTimeConf.script_font font_size));
menu#remove (redoMenuItem :> GMenu.menu_item);
MatitaGtkMisc.connect_menu_item new_redoMenuItem
(fun () -> self#safe_redo)));
menu#remove (redoMenuItem :> GMenu.menu_item);
MatitaGtkMisc.connect_menu_item new_redoMenuItem
(fun () -> self#safe_redo)));
(** text mark and tag representing locked part of a script *)
val locked_mark =
buffer#create_mark ~name:"locked" ~left_gravity:true buffer#start_iter
(** text mark and tag representing locked part of a script *)
val locked_mark =
buffer#create_mark ~name:"locked" ~left_gravity:true buffer#start_iter
let entries, newtext, parsed_len =
try
eval_statement self#include_paths buffer guistuff
let entries, newtext, parsed_len =
try
eval_statement self#include_paths buffer guistuff
- buffer#insert ~iter:(buffer#get_iter_at_mark (`MARK locked_mark)) newtext;
- (* here we need to set the Goal in case we are going to cursor (or to
- bottom) and we will face a macro *)
- userGoal <- None
+ buffer#insert ~iter:(buffer#get_iter_at_mark (`MARK locked_mark)) newtext
method private _retract offset grafite_status new_statements new_history =
NCicLibrary.time_travel grafite_status;
method private _retract offset grafite_status new_statements new_history =
NCicLibrary.time_travel grafite_status;
- let label = (MatitaMisc.get_gui ())#main#scriptLabel in
- label#set_text ((if b then "*" else "") ^ Filename.basename self#filename);
- label#misc#set_tooltip_text
- ("URI: " ^ self#buri_of_current_file ^ "\nPATH: " ^ self#filename)
+ tab_label#set_text ((if b then "*" else "")^Filename.basename self#filename);
+ tab_label#misc#set_tooltip_text
+ ("URI: " ^ self#buri_of_current_file ^ "\nPATH: " ^ self#filename);
method private reset_buffer =
statements <- [];
history <- [ initial_statuses (Some self#grafite_status) self#buri_of_current_file ];
method private reset_buffer =
statements <- [];
history <- [ initial_statuses (Some self#grafite_status) self#buri_of_current_file ];
self#notify;
buffer#remove_tag locked_tag ~start:buffer#start_iter ~stop:buffer#end_iter;
buffer#move_mark (`MARK locked_mark) ~where:buffer#start_iter
self#notify;
buffer#remove_tag locked_tag ~start:buffer#start_iter ~stop:buffer#end_iter;
buffer#move_mark (`MARK locked_mark) ~where:buffer#start_iter
let template = HExtlib.input_file BuildTimeConf.script_template in
buffer#insert ~iter:(buffer#get_iter `START) template;
buffer#set_modified false;
let template = HExtlib.input_file BuildTimeConf.script_template in
buffer#insert ~iter:(buffer#get_iter `START) template;
buffer#set_modified false;
HLog.debug (sprintf "%d statements:" (List.length statements));
List.iter HLog.debug statements;
HLog.debug ("Current file name: " ^ self#filename);
HLog.debug (sprintf "%d statements:" (List.length statements));
List.iter HLog.debug statements;
HLog.debug ("Current file name: " ^ self#filename);
-let current () = match !_script with None -> assert false | Some s -> s
+let at_page page =
+ let notebook = (MatitaMisc.get_gui ())#main#scriptNotebook in
+ let parent = notebook#get_nth_page page in
+ try
+ List.find (fun s -> s#has_parent parent) !_script
+ with
+ Not_found -> assert false
+;;
+
+let current () =
+ at_page ((MatitaMisc.get_gui ())#main#scriptNotebook#current_page)
+
+let iter_scripts f = List.iter f !_script;;