# HG changeset patch # User wenzelm # Date 1361965519 -3600 # Node ID 05b1bbae748db11ce9b9b8023eb38f199d31fc08 # Parent 8799eadf61fb668800e49b45bb351fbfb6ab081c discontinued obsolete 'uses' within theory header; diff -r 8799eadf61fb -r 05b1bbae748d NEWS --- a/NEWS Tue Feb 26 20:11:11 2013 +0100 +++ b/NEWS Wed Feb 27 12:45:19 2013 +0100 @@ -4,6 +4,13 @@ New in this Isabelle version ---------------------------- +*** General *** + +* Discontinued obsolete 'uses' within theory header. Note that +commands like 'ML_file' work without separate declaration of file +dependencies. Minor INCOMPATIBILITY. + + *** HOL *** * Discontinued obsolete src/HOL/IsaMakefile (considered legacy since diff -r 8799eadf61fb -r 05b1bbae748d etc/isar-keywords-ZF.el --- a/etc/isar-keywords-ZF.el Tue Feb 26 20:11:11 2013 +0100 +++ b/etc/isar-keywords-ZF.el Wed Feb 27 12:45:19 2013 +0100 @@ -249,7 +249,6 @@ "type_elims" "type_intros" "unchecked" - "uses" "where")) (defconst isar-keywords-control diff -r 8799eadf61fb -r 05b1bbae748d etc/isar-keywords.el --- a/etc/isar-keywords.el Tue Feb 26 20:11:11 2013 +0100 +++ b/etc/isar-keywords.el Wed Feb 27 12:45:19 2013 +0100 @@ -346,7 +346,6 @@ "structure" "unchecked" "unsafe" - "uses" "where")) (defconst isar-keywords-control diff -r 8799eadf61fb -r 05b1bbae748d src/HOL/Mirabelle/lib/scripts/mirabelle.pl --- a/src/HOL/Mirabelle/lib/scripts/mirabelle.pl Tue Feb 26 20:11:11 2013 +0100 +++ b/src/HOL/Mirabelle/lib/scripts/mirabelle.pl Wed Feb 27 12:45:19 2013 +0100 @@ -69,7 +69,7 @@ my $s = join ("\n", @action_files); my @action_files = split(/\n/, $s . "\n" . $s); %action_files = sort(@action_files); - $tools = "uses " . join(" ", sort(keys(%action_files))); + $tools = join("", map { "ML_file " . $_ . "\n" } (sort(keys(%action_files)))); } open(SETUP_FILE, ">$setup_file") || die "Could not create file '$setup_file'"; @@ -77,8 +77,9 @@ print SETUP_FILE < diff -r 8799eadf61fb -r 05b1bbae748d src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Tue Feb 26 20:11:11 2013 +0100 +++ b/src/Pure/PIDE/document.ML Wed Feb 27 12:45:19 2013 +0100 @@ -102,9 +102,9 @@ fun read_header node span = let - val (dir, {name = (name, _), imports, keywords, uses}) = get_header node; + val (dir, {name = (name, _), imports, keywords, files}) = get_header node; val {name = (_, pos), imports = imports', ...} = Thy_Header.read_tokens span; - in (dir, Thy_Header.make (name, pos) (map #1 imports ~~ map #2 imports') keywords uses) end; + in (dir, Thy_Header.make (name, pos) (map #1 imports ~~ map #2 imports') keywords files) end; fun get_perspective (Node {perspective, ...}) = perspective; fun set_perspective ids = diff -r 8799eadf61fb -r 05b1bbae748d src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Tue Feb 26 20:11:11 2013 +0100 +++ b/src/Pure/PIDE/document.scala Wed Feb 27 12:45:19 2013 +0100 @@ -40,7 +40,7 @@ sealed case class Header( imports: List[Name], keywords: Thy_Header.Keywords, - uses: List[(String, Boolean)], + files: List[String], errors: List[String] = Nil) { def error(msg: String): Header = copy(errors = errors ::: List(msg)) diff -r 8799eadf61fb -r 05b1bbae748d src/Pure/PIDE/protocol.ML --- a/src/Pure/PIDE/protocol.ML Tue Feb 26 20:11:11 2013 +0100 +++ b/src/Pure/PIDE/protocol.ML Wed Feb 27 12:45:19 2013 +0100 @@ -37,16 +37,16 @@ fn ([], a) => Document.Edits (list (pair (option int) (option int)) a), fn ([], a) => let - val (master, (name, (imports, (keywords, (uses, errors))))) = + val (master, (name, (imports, (keywords, (files, errors))))) = pair string (pair string (pair (list string) (pair (list (pair string (option (pair (pair string (list string)) (list string))))) - (pair (list (pair string bool)) (list string))))) a; + (pair (list string) (list string))))) a; val imports' = map (rpair Position.none) imports; - val (uses', errors') = - (map (apfst Path.explode) uses, errors) + val (files', errors') = + (map Path.explode files, errors) handle ERROR msg => ([], errors @ [msg]); - val header = Thy_Header.make (name, Position.none) imports' keywords uses'; + val header = Thy_Header.make (name, Position.none) imports' keywords files'; in Document.Deps (master, header, errors') end, fn (a, []) => Document.Perspective (map int_atom a)])) end; diff -r 8799eadf61fb -r 05b1bbae748d src/Pure/PIDE/protocol.scala --- a/src/Pure/PIDE/protocol.scala Tue Feb 26 20:11:11 2013 +0100 +++ b/src/Pure/PIDE/protocol.scala Wed Feb 27 12:45:19 2013 +0100 @@ -290,13 +290,13 @@ val imports = header.imports.map(_.node) val keywords = header.keywords.map({ case (a, b, _) => (a, b) }) // FIXME val uses = deps.uses.map(p => (Isabelle_System.posix_path(p._1), p._2)) - val uses = header.uses + val files = header.files (Nil, pair(Encode.string, pair(Encode.string, pair(list(Encode.string), pair(list(pair(Encode.string, option(pair(pair(Encode.string, list(Encode.string)), list(Encode.string))))), - pair(list(pair(Encode.string, bool)), list(Encode.string))))))( - (dir, (name.theory, (imports, (keywords, (uses, header.errors))))))) }, + pair(list(Encode.string), list(Encode.string))))))( + (dir, (name.theory, (imports, (keywords, (files, header.errors))))))) }, { case Document.Node.Perspective(a) => (a.commands.map(c => long_atom(c.id)), Nil) })) def encode_edits: T[List[Document.Edit_Command]] = list((node_edit: Document.Edit_Command) => { diff -r 8799eadf61fb -r 05b1bbae748d src/Pure/ProofGeneral/proof_general_pgip.ML --- a/src/Pure/ProofGeneral/proof_general_pgip.ML Tue Feb 26 20:11:11 2013 +0100 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Wed Feb 27 12:45:19 2013 +0100 @@ -592,10 +592,9 @@ fun filerefs f = let val thy = thy_name f - 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}) + name=NONE, idtables=[], fileurls=[]}) end fun thyrefs thy = diff -r 8799eadf61fb -r 05b1bbae748d src/Pure/Pure.thy --- a/src/Pure/Pure.thy Tue Feb 26 20:11:11 2013 +0100 +++ b/src/Pure/Pure.thy Wed Feb 27 12:45:19 2013 +0100 @@ -12,8 +12,7 @@ "attach" "begin" "binder" "constrains" "defines" "fixes" "for" "identifier" "if" "imports" "in" "includes" "infix" "infixl" "infixr" "is" "keywords" "notes" "obtains" "open" "output" - "overloaded" "pervasive" "shows" "structure" "unchecked" "uses" - "where" "|" + "overloaded" "pervasive" "shows" "structure" "unchecked" "where" "|" and "header" :: diag and "chapter" :: thy_heading1 and "section" :: thy_heading2 diff -r 8799eadf61fb -r 05b1bbae748d src/Pure/Thy/present.ML --- a/src/Pure/Thy/present.ML Tue Feb 26 20:11:11 2013 +0100 +++ b/src/Pure/Thy/present.ML Wed Feb 27 12:45:19 2013 +0100 @@ -21,7 +21,7 @@ val init_theory: string -> unit val theory_source: string -> (unit -> HTML.text) -> unit val theory_output: string -> string -> unit - val begin_theory: int -> Path.T -> (Path.T * bool) list -> theory -> theory + val begin_theory: int -> Path.T -> theory -> theory val drafts: string -> Path.T list -> Path.T end; @@ -451,13 +451,14 @@ else Url.File (Path.append (mk_rel_path curr_session session) (html_path name))); in (link, name) end; -fun begin_theory update_time dir files thy = +fun begin_theory update_time dir thy = session_default thy (fn {name = sess_name, session, path, html_prefix, remote_path, ...} => let val name = Context.theory_name thy; val parents = Theory.parents_of thy; val parent_specs = map (parent_link remote_path path) parents; + val files = []; (* FIXME *) val files_html = files |> map (fn (raw_path, loadit) => let val path = File.check_file (File.full_path dir raw_path); diff -r 8799eadf61fb -r 05b1bbae748d src/Pure/Thy/thy_header.ML --- a/src/Pure/Thy/thy_header.ML Tue Feb 26 20:11:11 2013 +0100 +++ b/src/Pure/Thy/thy_header.ML Wed Feb 27 12:45:19 2013 +0100 @@ -11,9 +11,8 @@ {name: string * Position.T, imports: (string * Position.T) list, keywords: keywords, - uses: (Path.T * bool) list} - val make: string * Position.T -> (string * Position.T) list -> keywords -> - (Path.T * bool) list -> header + files: Path.T list} + val make: string * Position.T -> (string * Position.T) list -> keywords -> Path.T list -> header val define_keywords: header -> unit val declare_keyword: string * Keyword.spec option -> theory -> theory val the_keyword: theory -> string -> Keyword.spec option @@ -31,10 +30,10 @@ {name: string * Position.T, imports: (string * Position.T) list, keywords: keywords, - uses: (Path.T * bool) list}; + files: Path.T list}; -fun make name imports keywords uses : header = - {name = name, imports = imports, keywords = keywords, uses = uses}; +fun make name imports keywords files : header = + {name = name, imports = imports, keywords = keywords, files = files}; @@ -73,12 +72,11 @@ val theoryN = "theory"; val importsN = "imports"; val keywordsN = "keywords"; -val usesN = "uses"; val beginN = "begin"; val header_lexicons = pairself (Scan.make_lexicon o map Symbol.explode) - (["%", "(", ")", ",", "::", ";", "==", "and", beginN, importsN, keywordsN, usesN], + (["%", "(", ")", ",", "::", ";", "==", "and", beginN, importsN, keywordsN], [headerN, theoryN]); @@ -86,7 +84,6 @@ local -val file_name = Parse.group (fn () => "file name") Parse.path >> Path.explode; val theory_name = Parse.group (fn () => "theory name") (Parse.position Parse.name); val opt_files = @@ -107,19 +104,14 @@ val keyword_decls = Parse.and_list1 keyword_decl >> flat; -val file = - Parse.$$$ "(" |-- Parse.!!! (file_name --| Parse.$$$ ")") >> rpair false || - file_name >> rpair true; - in val args = theory_name -- Scan.optional (Parse.$$$ importsN |-- Parse.!!! (Scan.repeat1 theory_name)) [] -- - Scan.optional (Parse.$$$ keywordsN |-- Parse.!!! keyword_decls) [] -- - Scan.optional (Parse.$$$ usesN |-- Parse.!!! (Scan.repeat1 file)) [] --| + Scan.optional (Parse.$$$ keywordsN |-- Parse.!!! keyword_decls) [] --| Parse.$$$ beginN >> - (fn (((name, imports), keywords), uses) => make name imports keywords uses); + (fn ((name, imports), keywords) => make name imports keywords []); end; diff -r 8799eadf61fb -r 05b1bbae748d src/Pure/Thy/thy_header.scala --- a/src/Pure/Thy/thy_header.scala Tue Feb 26 20:11:11 2013 +0100 +++ b/src/Pure/Thy/thy_header.scala Wed Feb 27 12:45:19 2013 +0100 @@ -22,12 +22,11 @@ val IMPORTS = "imports" val KEYWORDS = "keywords" val AND = "and" - val USES = "uses" val BEGIN = "begin" private val lexicon = Scan.Lexicon("%", "(", ")", ",", "::", ";", "==", - AND, BEGIN, HEADER, IMPORTS, KEYWORDS, THEORY, USES) + AND, BEGIN, HEADER, IMPORTS, KEYWORDS, THEORY) /* theory file name */ @@ -72,9 +71,8 @@ theory_name ~ (opt(keyword(IMPORTS) ~! (rep1(theory_name))) ^^ { case None => Nil case Some(_ ~ xs) => xs }) ~ (opt(keyword(KEYWORDS) ~! keyword_decls) ^^ { case None => Nil case Some(_ ~ xs) => xs }) ~ - (opt(keyword(USES) ~! (rep1(file))) ^^ { case None => Nil case Some(_ ~ xs) => xs }) ~ keyword(BEGIN) ^^ - { case x ~ ys ~ zs ~ ws ~ _ => Thy_Header(x, ys, zs, ws) } + { case x ~ ys ~ zs ~ _ => Thy_Header(x, ys, zs, Nil) } (keyword(HEADER) ~ tags) ~! ((doc_source ~ rep(keyword(";")) ~ keyword(THEORY) ~ tags) ~> args) ^^ { case _ ~ x => x } | @@ -120,9 +118,9 @@ name: String, imports: List[String], keywords: Thy_Header.Keywords, - uses: List[(String, Boolean)]) + files: List[String]) { def map(f: String => String): Thy_Header = - Thy_Header(f(name), imports.map(f), keywords, uses.map(p => (f(p._1), p._2))) + Thy_Header(f(name), imports.map(f), keywords, files.map(f)) } diff -r 8799eadf61fb -r 05b1bbae748d src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML Tue Feb 26 20:11:11 2013 +0100 +++ b/src/Pure/Thy/thy_info.ML Wed Feb 27 12:45:19 2013 +0100 @@ -235,7 +235,7 @@ fun required_by _ [] = "" | required_by s initiators = s ^ "(required by " ^ show_path (rev initiators) ^ ")"; -fun load_thy last_timing initiators update_time deps text (name, pos) uses keywords parents = +fun load_thy last_timing initiators update_time deps text (name, pos) keywords parents = let val _ = kill_thy name; val _ = Output.urgent_message ("Loading theory " ^ quote name ^ required_by " " initiators); @@ -243,7 +243,7 @@ val {master = (thy_path, _), imports} = deps; val dir = Path.dir thy_path; - val header = Thy_Header.make (name, pos) imports keywords uses; + val header = Thy_Header.make (name, pos) imports keywords []; val _ = Position.reports (map #2 imports ~~ map Theory.get_markup parents); @@ -257,21 +257,21 @@ fun check_deps dir name = (case lookup_deps name of - SOME NONE => (true, NONE, Position.none, get_imports name, [], []) + SOME NONE => (true, NONE, Position.none, get_imports name, []) | NONE => - let val {master, text, theory_pos, imports, keywords, uses} = Thy_Load.check_thy dir name - in (false, SOME (make_deps master imports, text), theory_pos, imports, uses, keywords) end + let val {master, text, theory_pos, imports, keywords} = Thy_Load.check_thy dir name + in (false, SOME (make_deps master imports, text), theory_pos, imports, keywords) end | SOME (SOME {master, ...}) => let val {master = master', text = text', theory_pos = theory_pos', imports = imports', - uses = uses', keywords = keywords'} = Thy_Load.check_thy dir name; + keywords = keywords'} = Thy_Load.check_thy dir name; val deps' = SOME (make_deps master' imports', text'); val current = #2 master = #2 master' andalso (case lookup_theory name of NONE => false | SOME theory => Thy_Load.load_current theory); - in (current, deps', theory_pos', imports', uses', keywords') end); + in (current, deps', theory_pos', imports', keywords') end); in @@ -289,7 +289,7 @@ val dir' = Path.append dir (Path.dir path); val _ = member (op =) initiators name andalso error (cycle_msg initiators); - val (current, deps, theory_pos, imports, uses, keywords) = check_deps dir' name + val (current, deps, theory_pos, imports, keywords) = check_deps dir' name handle ERROR msg => cat_error msg (loader_msg "the error(s) above occurred while examining theory" [name] ^ Position.here require_pos ^ required_by "\n" initiators); @@ -310,7 +310,7 @@ val update_time = serial (); val load = load_thy last_timing initiators update_time dep - text (name, theory_pos) uses keywords; + text (name, theory_pos) keywords; in Task (parents, load) end); val tasks'' = new_entry name parents task tasks'; diff -r 8799eadf61fb -r 05b1bbae748d src/Pure/Thy/thy_info.scala --- a/src/Pure/Thy/thy_info.scala Tue Feb 26 20:11:11 2013 +0100 +++ b/src/Pure/Thy/thy_info.scala Wed Feb 27 12:45:19 2013 +0100 @@ -94,7 +94,7 @@ Library.future_value(Exn.capture { try { val files = thy_load.body_files(syntax0, string) - header0.copy(uses = header0.uses ::: files.map((_, false))) + header0.copy(files = header0.files ::: files) } catch { case ERROR(msg) => err(msg) } }) diff -r 8799eadf61fb -r 05b1bbae748d src/Pure/Thy/thy_load.ML --- a/src/Pure/Thy/thy_load.ML Tue Feb 26 20:11:11 2013 +0100 +++ b/src/Pure/Thy/thy_load.ML Wed Feb 27 12:45:19 2013 +0100 @@ -12,7 +12,7 @@ val parse_files: string -> (theory -> Token.file list) parser val check_thy: Path.T -> string -> {master: Path.T * SHA1.digest, text: string, theory_pos: Position.T, - imports: (string * Position.T) list, uses: (Path.T * bool) list, keywords: Thy_Header.keywords} + imports: (string * Position.T) list, keywords: Thy_Header.keywords} val provide: Path.T * SHA1.digest -> theory -> theory val provide_parse_files: string -> (theory -> Token.file list * theory) parser val load_file: theory -> Path.T -> (Path.T * SHA1.digest) * string @@ -132,13 +132,13 @@ val master_file = check_file dir path; val text = File.read master_file; - val {name = (name, pos), imports, uses, keywords} = + val {name = (name, pos), imports, files = [], 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 ^ Position.here pos); in {master = (master_file, SHA1.digest text), text = text, theory_pos = pos, - imports = imports, uses = uses, keywords = keywords} + imports = imports, keywords = keywords} end; @@ -207,11 +207,10 @@ (* load_thy *) -fun begin_theory master_dir {name, imports, keywords, uses} parents = +fun begin_theory master_dir {name, imports, keywords, files = []} parents = Theory.begin_theory name parents |> put_deps master_dir imports |> fold Thy_Header.declare_keyword keywords - |> fold (fn (path, true) => Context.theory_map (exec_ml path) o Theory.checkpoint | _ => I) uses |> Theory.checkpoint; fun excursion last_timing init elements = @@ -239,12 +238,12 @@ let val time = ! Toplevel.timing; - val {name = (name, _), uses, ...} = header; + val {name = (name, _), files = [], ...} = header; val _ = Thy_Header.define_keywords header; val _ = Present.init_theory name; fun init () = begin_theory master_dir header parents - |> Present.begin_theory update_time master_dir uses; + |> Present.begin_theory update_time master_dir; val lexs = Keyword.get_lexicons (); diff -r 8799eadf61fb -r 05b1bbae748d src/Pure/Thy/thy_load.scala --- a/src/Pure/Thy/thy_load.scala Tue Feb 26 20:11:11 2013 +0100 +++ b/src/Pure/Thy/thy_load.scala Wed Feb 27 12:45:19 2013 +0100 @@ -114,8 +114,7 @@ " for theory " + quote(name1)) val imports = header.imports.map(import_name(name.dir, _)) - val uses = header.uses - Document.Node.Header(imports, header.keywords, uses) + Document.Node.Header(imports, header.keywords, Nil) } catch { case exn: Throwable => Document.Node.bad_header(Exn.message(exn)) } } diff -r 8799eadf61fb -r 05b1bbae748d src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Tue Feb 26 20:11:11 2013 +0100 +++ b/src/Pure/Tools/build.scala Wed Feb 27 12:45:19 2013 +0100 @@ -417,9 +417,9 @@ val all_files = (thy_deps.deps.map({ case dep => val thy = Path.explode(dep.name.node) - val uses = dep.join_header.uses.map(p => - Path.explode(dep.name.dir) + Path.explode(p._1)) - thy :: uses + val files = dep.join_header.files.map(file => + Path.explode(dep.name.dir) + Path.explode(file)) + thy :: files }).flatten ::: info.files.map(file => info.dir + file)).map(_.expand) if (list_files)