--- 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
--- 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
--- 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
--- 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 <<END;
theory "$setup_thy_name"
imports "$mirabelle_thy" "$mirabelle_theory"
+begin
+
$tools
-begin
setup {*
Config.put_global Mirabelle.logfile "$log_file" #>
--- 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 =
--- 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))
--- 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;
--- 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) =>
{
--- 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 =
--- 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
--- 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);
--- 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;
--- 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))
}
--- 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';
--- 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) }
})
--- 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 ();
--- 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)) }
}
--- 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)