parsed_text st
=
let module TAPp = GrafiteAstPp in
- let include_ =
- match guistuff.filenamedata with
- | None,None -> []
- | None,Some devel -> [MatitamakeLib.root_for_development devel ]
- | Some f,_ ->
- match MatitamakeLib.development_for_dir (Filename.dirname f) with
- | None -> []
- | Some devel -> [MatitamakeLib.root_for_development devel ]
- in
- let include_ =
- include_ @ (Helm_registry.get_list Helm_registry.string "matita.includes")
- in
let parsed_text_length = String.length parsed_text in
let loc, ex =
match st with TA.Executable (loc,ex) -> loc, ex | _ -> assert false in
GrafiteAstPp.pp_statement ~term_pp:CicNotationPp.pp_term
~lazy_term_pp:(fun _ -> assert false) ~obj_pp:(fun _ -> assert false)
-let rec eval_macro (buffer : GText.buffer) guistuff lexicon_status grafite_status user_goal unparsed_text parsed_text script mac =
+let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status grafite_status user_goal unparsed_text parsed_text script mac =
let module TAPp = GrafiteAstPp in
let module MQ = MetadataQuery in
let module MDB = LibraryDb in
let loc = HExtlib.floc_of_loc (0,text_len) in
let statement = `Ast (GrafiteParser.LSome (ast loc),text) in
let res,_parsed_text_len =
- eval_statement buffer guistuff lexicon_status grafite_status
- user_goal script statement
+ eval_statement include_paths buffer guistuff lexicon_status
+ grafite_status user_goal script statement
in
(* we need to replace all the parsed_text *)
res,String.length parsed_text
| TA.Search_pat (_, search_kind, str) -> failwith "not implemented"
| TA.Search_term (_, search_kind, term) -> failwith "not implemented"
-and eval_executable (buffer : GText.buffer) guistuff lexicon_status grafite_status user_goal unparsed_text parsed_text script loc ex
+and eval_executable include_paths (buffer : GText.buffer) guistuff lexicon_status grafite_status user_goal unparsed_text parsed_text script loc ex
=
let module TAPp = GrafiteAstPp in
let module MD = GrafiteDisambiguator in
None -> []
| Some n -> GrafiteTypes.get_proof_context grafite_status n in
let grafite_status,macro = lazy_macro context in
- eval_macro buffer guistuff lexicon_status grafite_status user_goal
- unparsed_text parsed_text script macro
+ eval_macro include_paths buffer guistuff lexicon_status grafite_status
+ user_goal unparsed_text parsed_text script macro
-and eval_statement (buffer : GText.buffer) guistuff lexicon_status
+and eval_statement include_paths (buffer : GText.buffer) guistuff lexicon_status
grafite_status user_goal script statement
=
let (lexicon_status,st), unparsed_text =
| `Raw text ->
if Pcre.pmatch ~rex:only_dust_RE text then raise Margin;
GrafiteParser.parse_statement (Ulexing.from_utf8_string text)
- ~include_paths:(Helm_registry.get_list
- Helm_registry.string "matita.includes")
- lexicon_status, text
+ ~include_paths lexicon_status, text
| `Ast (st, text) -> (lexicon_status, st), text
in
let text_of_loc loc =
let s = String.sub unparsed_text parsed_text_length remain_len in
let s,len =
try
- eval_statement buffer guistuff lexicon_status grafite_status user_goal
- script (`Raw s)
+ eval_statement include_paths buffer guistuff lexicon_status
+ grafite_status user_goal script (`Raw s)
with
HExtlib.Localized (floc, exn) ->
HExtlib.raise_localized_exception ~offset:parsed_text_length floc exn
| [] -> [], 0)
| GrafiteParser.LSome (GrafiteAst.Executable (loc, ex)) ->
let parsed_text, parsed_text_length = text_of_loc loc in
- eval_executable buffer guistuff lexicon_status grafite_status user_goal
- unparsed_text parsed_text script loc ex
+ eval_executable include_paths buffer guistuff lexicon_status
+ grafite_status user_goal unparsed_text parsed_text script loc ex
let fresh_script_id =
let i = ref 0 in
let buffer = source_view#buffer in
let source_buffer = source_view#source_buffer in
let initial_statuses =
+ (* 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 =
grafite_status,lexicon_status
in
object (self)
+ val mutable include_paths =
+ Helm_registry.get_list Helm_registry.string "matita.includes"
+
val scriptId = fresh_script_id ()
val guistuff = {
HLog.debug ("evaluating: " ^ first_line s ^ " ...");
let (entries, parsed_len) =
try
- eval_statement buffer guistuff self#lexicon_status self#grafite_status
- userGoal self (`Raw s)
+ eval_statement include_paths buffer guistuff self#lexicon_status
+ self#grafite_status userGoal self (`Raw s)
with End_of_file -> raise Margin
in
let new_statuses, new_statements =
method assignFileName file =
let abspath = MatitaMisc.absolute_path file in
- let devel = MatitamakeLib.development_for_dir (Filename.dirname abspath) in
- guistuff.filenamedata <- Some abspath, devel
+ let dirname = Filename.dirname abspath in
+ let devel = MatitamakeLib.development_for_dir dirname in
+ guistuff.filenamedata <- Some abspath, devel;
+ let include_ =
+ match MatitamakeLib.development_for_dir dirname with
+ None -> []
+ | Some devel -> [MatitamakeLib.root_for_development devel] in
+ let include_ =
+ include_ @ (Helm_registry.get_list Helm_registry.string "matita.includes")
+ in
+ include_paths <- include_
method saveToFile () =
let oc = open_out self#getFilename in
method template () =
let template = HExtlib.input_file BuildTimeConf.script_template in
buffer#insert ~iter:(buffer#get_iter `START) template;
- guistuff.filenamedata <-
- (None,MatitamakeLib.development_for_dir (Unix.getcwd ()));
- buffer#set_modified false;
- set_star (Filename.basename self#ppFilename) false
+ let development = MatitamakeLib.development_for_dir (Unix.getcwd ()) in
+ guistuff.filenamedata <- (None,development);
+ let include_ =
+ match development with
+ None -> []
+ | Some devel -> [MatitamakeLib.root_for_development devel ]
+ in
+ let include_ =
+ include_ @ (Helm_registry.get_list Helm_registry.string "matita.includes")
+ in
+ include_paths <- include_ ;
+ buffer#set_modified false;
+ set_star (Filename.basename self#ppFilename) false
method goto (pos: [`Top | `Bottom | `Cursor]) () =
let old_locked_mark =
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:(Helm_registry.get_list
- Helm_registry.string "matita.includes")
- lexicon_status
+ ~include_paths lexicon_status
in
match st with
GrafiteParser.LNone loc
projects / helm.git / blobdiff