From 0767097b6f841f43d033b54b262e88423aef7da9 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sun, 8 Jan 2006 19:16:27 +0000 Subject: [PATCH] Bug fixed: the include_paths were no longer handled properly when matita was launched outside a development. E.g.: ./matita library/nat/times.ma was no longer working (./matita -I library library/nat/times.ma was) --- helm/matita/matitaScript.ml | 80 ++++++++++++++++++++----------------- 1 file changed, 43 insertions(+), 37 deletions(-) diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml index a0d0944ca..d628af98d 100644 --- a/helm/matita/matitaScript.ml +++ b/helm/matita/matitaScript.ml @@ -79,18 +79,6 @@ let eval_with_engine guistuff lexicon_status grafite_status user_goal 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 @@ -215,7 +203,7 @@ let pp_eager_statement_ast = 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 @@ -290,8 +278,8 @@ let rec eval_macro (buffer : GText.buffer) guistuff lexicon_status grafite_statu 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 @@ -318,7 +306,7 @@ let rec eval_macro (buffer : GText.buffer) guistuff lexicon_status grafite_statu | 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 @@ -354,10 +342,10 @@ and eval_executable (buffer : GText.buffer) guistuff lexicon_status grafite_stat 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 = @@ -365,9 +353,7 @@ and eval_statement (buffer : GText.buffer) guistuff lexicon_status | `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 = @@ -386,8 +372,8 @@ and eval_statement (buffer : GText.buffer) guistuff lexicon_status 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 @@ -402,8 +388,8 @@ and eval_statement (buffer : GText.buffer) guistuff lexicon_status | [] -> [], 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 @@ -419,6 +405,7 @@ class script ~(source_view: GSourceView.source_view) 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 = @@ -428,6 +415,9 @@ let initial_statuses = 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 = { @@ -484,8 +474,8 @@ object (self) 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 = @@ -598,8 +588,17 @@ object (self) 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 @@ -650,10 +649,19 @@ object (self) 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 = @@ -767,9 +775,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:(Helm_registry.get_list - Helm_registry.string "matita.includes") - lexicon_status + ~include_paths lexicon_status in match st with GrafiteParser.LNone loc -- 2.39.2