X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fmatita%2FmatitaScript.ml;h=4c53f113bd9d0db4b7707d628a320be84f00dee8;hb=9ffc433e8913660620b1dd4ce4c22db1e42c7562;hp=a0d0944ca0c8d770375b8395db59c6a211225b54;hpb=e66e67d2f9f2772d63a7457e386f9616f62a2f39;p=helm.git diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml index a0d0944ca..4c53f113b 100644 --- a/helm/matita/matitaScript.ml +++ b/helm/matita/matitaScript.ml @@ -79,21 +79,7 @@ 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 let initial_space,parsed_text = try let pieces = Pcre.extract ~rex:heading_nl_RE' parsed_text in @@ -103,7 +89,9 @@ let eval_with_engine guistuff lexicon_status grafite_status user_goal let inital_space,new_grafite_status,new_lexicon_status,new_status_and_text_list' = (* the code commented out adds the "select" command if needed *) initial_space,grafite_status,lexicon_status,[] in -(* match grafite_status.proof_status with +(* let loc, ex = + match st with TA.Executable (loc,ex) -> loc, ex | _ -> assert false in + match grafite_status.proof_status with | Incomplete_proof { stack = stack } when not (List.mem user_goal (Continuationals.head_goals stack)) -> let grafite_status = @@ -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 = @@ -747,9 +755,8 @@ object (self) method proofContext = match userGoal with - None -> assert false - | Some n -> - GrafiteTypes.get_proof_context self#grafite_status n + None -> [] + | Some n -> GrafiteTypes.get_proof_context self#grafite_status n method proofConclusion = match userGoal with @@ -758,7 +765,7 @@ object (self) GrafiteTypes.get_proof_conclusion self#grafite_status n method stack = GrafiteTypes.get_stack self#grafite_status - method setGoal n = userGoal <- Some n + method setGoal n = userGoal <- n method goal = userGoal method eos = @@ -767,9 +774,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