# HG changeset patch # User wenzelm # Date 1345718022 -7200 # Node ID 9fc880720663e76420de1b5275f0c33b69f9465f # Parent 873fdafc5b0948c659755f3b10776404381fd476 simplified Thy_Load.check_thy (again) -- no need to pass keywords nor find files in body text; diff -r 873fdafc5b09 -r 9fc880720663 src/Pure/Isar/keyword.ML --- a/src/Pure/Isar/keyword.ML Thu Aug 23 12:00:11 2012 +0200 +++ b/src/Pure/Isar/keyword.ML Thu Aug 23 12:33:42 2012 +0200 @@ -57,7 +57,6 @@ val command_tags: string -> string list val dest: unit -> string list * string list val status: unit -> unit - val thy_load_commands: keywords -> (string * string list) list val define_keywords: string * T option -> keywords -> keywords val define: string * T option -> unit val is_diag: string -> bool @@ -221,11 +220,6 @@ in () end; -fun thy_load_commands (Keywords {commands, ...}) = - Symtab.fold (fn (name, Keyword {kind, files, ...}) => - kind = kind_of thy_load ? cons (name, files)) commands []; - - (* define *) fun define_keywords (name, opt_kind) = map_keywords (fn ((minor, major), commands) => diff -r 873fdafc5b09 -r 9fc880720663 src/Pure/ProofGeneral/proof_general_pgip.ML --- a/src/Pure/ProofGeneral/proof_general_pgip.ML Thu Aug 23 12:00:11 2012 +0200 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Thu Aug 23 12:33:42 2012 +0200 @@ -594,14 +594,14 @@ fun filerefs f = let val thy = thy_name f - val filerefs = map #1 (#uses (Thy_Load.check_thy [] (Path.dir f) thy)) + val filerefs = map #1 (#uses (Thy_Load.check_thy (Path.dir f) thy)) in issue_pgip (Setrefs {url=url, thyname=NONE, objtype=SOME PgipTypes.ObjFile, name=NONE, idtables=[], fileurls=filerefs}) end fun thyrefs thy = - let val thyrefs = #imports (Thy_Load.check_thy [] Path.current thy) + let val thyrefs = #imports (Thy_Load.check_thy Path.current thy) in issue_pgip (Setrefs {url=url, thyname=thyname, objtype=SOME PgipTypes.ObjTheory, name=NONE, idtables=[{context=NONE, objtype=PgipTypes.ObjTheory, diff -r 873fdafc5b09 -r 9fc880720663 src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML Thu Aug 23 12:00:11 2012 +0200 +++ b/src/Pure/Thy/thy_info.ML Thu Aug 23 12:33:42 2012 +0200 @@ -236,16 +236,16 @@ fun commit () = update_thy deps theory; in (theory, present, commit) end; -fun check_deps base_keywords dir name = +fun check_deps dir name = (case lookup_deps name of SOME NONE => (true, NONE, get_imports name, [], []) | NONE => - let val {master, text, imports, keywords, uses} = Thy_Load.check_thy base_keywords dir name + let val {master, text, imports, keywords, uses} = Thy_Load.check_thy dir name in (false, SOME (make_deps master imports, text), imports, uses, keywords) end | SOME (SOME {master, ...}) => let val {master = master', text = text', imports = imports', uses = uses', keywords = keywords'} - = Thy_Load.check_thy base_keywords dir name; + = Thy_Load.check_thy dir name; val deps' = SOME (make_deps master' imports', text'); val current = #2 master = #2 master' andalso @@ -256,29 +256,29 @@ in -fun require_thys initiators dir strs result = - fold_map (require_thy initiators dir) strs result |>> forall I -and require_thy initiators dir str (base_keywords, tasks) = +fun require_thys initiators dir strs tasks = + fold_map (require_thy initiators dir) strs tasks |>> forall I +and require_thy initiators dir str tasks = let val path = Path.expand (Path.explode str); val name = Path.implode (Path.base path); in (case try (Graph.get_node tasks) name of - SOME task => (task_finished task, (base_keywords, tasks)) + SOME task => (task_finished task, tasks) | NONE => let val dir' = Path.append dir (Path.dir path); val _ = member (op =) initiators name andalso error (cycle_msg initiators); - val (current, deps, imports, uses, keywords) = check_deps base_keywords dir' name + val (current, deps, imports, uses, keywords) = check_deps dir' name handle ERROR msg => cat_error msg (loader_msg "the error(s) above occurred while examining theory" [name] ^ required_by "\n" initiators); val parents = map base_name imports; - val (parents_current, (base_keywords', tasks')) = + val (parents_current, tasks') = require_thys (name :: initiators) - (Path.append dir (master_dir (Option.map #1 deps))) imports (base_keywords, tasks); + (Path.append dir (master_dir (Option.map #1 deps))) imports tasks; val all_current = current andalso parents_current; val task = @@ -292,9 +292,8 @@ val load = load_thy initiators update_time dep text name uses keywords; in Task (parents, load) end); - val base_keywords'' = keywords @ base_keywords'; val tasks'' = new_entry name parents task tasks'; - in (all_current, (base_keywords'', tasks'')) end) + in (all_current, tasks'') end) end; end; @@ -303,7 +302,7 @@ (* use_thy *) fun use_thys_wrt dir arg = - schedule_tasks (snd (snd (require_thys [] dir arg ([], Graph.empty)))); + schedule_tasks (snd (require_thys [] dir arg Graph.empty)); val use_thys = use_thys_wrt Path.current; val use_thy = use_thys o single; @@ -326,7 +325,7 @@ fun register_thy theory = let val name = Context.theory_name theory; - val {master, ...} = Thy_Load.check_thy [] (Thy_Load.master_directory theory) name; + val {master, ...} = Thy_Load.check_thy (Thy_Load.master_directory theory) name; val imports = Thy_Load.imports_of theory; in NAMED_CRITICAL "Thy_Info" (fn () => diff -r 873fdafc5b09 -r 9fc880720663 src/Pure/Thy/thy_load.ML --- a/src/Pure/Thy/thy_load.ML Thu Aug 23 12:00:11 2012 +0200 +++ b/src/Pure/Thy/thy_load.ML Thu Aug 23 12:33:42 2012 +0200 @@ -10,7 +10,7 @@ val imports_of: theory -> string list val provide: Path.T * SHA1.digest -> theory -> theory val thy_path: Path.T -> Path.T - val check_thy: Thy_Header.keywords -> Path.T -> string -> + val check_thy: Path.T -> string -> {master: Path.T * SHA1.digest, text: string, imports: string list, uses: (Path.T * bool) list, keywords: Thy_Header.keywords} val load_file: theory -> Path.T -> (Path.T * SHA1.digest) * string @@ -69,6 +69,21 @@ fun check_file dir file = File.check_file (File.full_path dir file); +fun read_files cmd dir path = + let + val paths = + (case Keyword.command_files cmd of + [] => [path] + | exts => map (fn ext => Path.ext ext path) exts); + val files = paths |> map (check_file dir #> (fn p => (File.read p, Path.position p))); + in (dir, files) end; + +fun parse_files cmd = + Scan.ahead Parse.not_eof -- Parse.path >> (fn (tok, name) => fn thy => + (case Token.get_files tok of + SOME files => files + | NONE => read_files cmd (master_directory thy) (Path.explode name))); + local fun clean ((i1, t1) :: (i2, t2) :: toks) = @@ -88,42 +103,8 @@ handle ERROR msg => error (msg ^ Token.pos_of tok) else NONE); -fun command_files path exts = - if null exts then [path] - else map (fn ext => Path.ext ext path) exts; - in -fun find_files syntax text = - let val thy_load_commands = Keyword.thy_load_commands syntax in - if exists (fn (cmd, _) => String.isSubstring cmd text) thy_load_commands then - Thy_Syntax.parse_tokens (Keyword.lexicons_of syntax) Position.none text - |> Thy_Syntax.parse_spans - |> maps - (fn Thy_Syntax.Span (Thy_Syntax.Command (cmd, _), toks) => - (case AList.lookup (op =) thy_load_commands cmd of - SOME exts => - (case find_file toks of - SOME (_, path) => command_files path exts - | NONE => []) - | NONE => []) - | _ => []) - else [] - end; - -fun read_files cmd dir path = - let - val files = - command_files path (Keyword.command_files cmd) - |> map (check_file dir #> (fn p => (File.read p, Path.position p))); - in (dir, files) end; - -fun parse_files cmd = - Scan.ahead Parse.not_eof -- Parse.path >> (fn (tok, name) => fn thy => - (case Token.get_files tok of - SOME files => files - | NONE => read_files cmd (master_directory thy) (Path.explode name))); - fun resolve_files master_dir span = (case span of Thy_Syntax.Span (Thy_Syntax.Command (cmd, pos), toks) => @@ -146,7 +127,7 @@ val thy_path = Path.ext "thy"; -fun check_thy base_keywords dir thy_name = +fun check_thy dir thy_name = let val path = thy_path (Path.basic thy_name); val master_file = check_file dir path; @@ -155,14 +136,9 @@ val {name, imports, uses, keywords} = Thy_Header.read (Path.position master_file) text; val _ = thy_name <> name andalso error ("Bad file name " ^ Path.print path ^ " for theory " ^ quote name); - - val syntax = - fold (Keyword.define_keywords o apsnd (Option.map Keyword.spec)) - (keywords @ base_keywords) (Keyword.get_keywords ()); - val more_uses = map (rpair false) (find_files syntax text); in {master = (master_file, SHA1.digest text), text = text, - imports = imports, uses = uses @ more_uses, keywords = keywords} + imports = imports, uses = uses, keywords = keywords} end;