--- a/NEWS Fri Jul 23 10:58:13 2010 +0200
+++ b/NEWS Fri Jul 23 18:42:46 2010 +0200
@@ -14,6 +14,11 @@
consistent view on symbols, while raw explode (or String.explode)
merely give a byte-oriented representation.
+* Special treatment of ML file names has been discontinued.
+Historically, optional extensions .ML or .sml were added on demand --
+at the cost of clarity of file dependencies. Recall that Isabelle/ML
+files exclusively use the .ML extension. Minor INCOMPATIBILTY.
+
*** HOL ***
--- a/lib/html/isabelle.css Fri Jul 23 10:58:13 2010 +0200
+++ b/lib/html/isabelle.css Fri Jul 23 18:42:46 2010 +0200
@@ -5,8 +5,8 @@
.head { background-color: #FFFFFF; }
.source { background-color: #F0F0F0; padding: 10px; }
-.mlsource { background-color: #F0F0F0; padding: 10px; }
-.mlfooter { background-color: #FFFFFF; }
+.external_source { background-color: #F0F0F0; padding: 10px; }
+.external_footer { background-color: #FFFFFF; }
.theories { background-color: #F0F0F0; padding: 10px; }
.sessions { background-color: #F0F0F0; padding: 10px; }
@@ -14,9 +14,6 @@
.name { font-style: italic; }
.filename { font-family: fixed; }
-/* hide hr for this style */
-hr { height: 0px; border: 0px; }
-
/* basic syntax markup */
--- a/src/HOL/Boogie/Tools/boogie_commands.ML Fri Jul 23 10:58:13 2010 +0200
+++ b/src/HOL/Boogie/Tools/boogie_commands.ML Fri Jul 23 18:42:46 2010 +0200
@@ -268,7 +268,7 @@
val _ =
Outer_Syntax.command "boogie_open"
- "Open a new Boogie environment and load a Boogie-generated .b2i file."
+ "open a new Boogie environment and load a Boogie-generated .b2i file"
Keyword.thy_decl
(scan_opt "quiet" -- Parse.name -- vc_offsets >>
(Toplevel.theory o boogie_open))
@@ -296,7 +296,7 @@
val _ =
Outer_Syntax.command "boogie_vc"
- "Enter into proof mode for a specific verification condition."
+ "enter into proof mode for a specific verification condition"
Keyword.thy_goal
(vc_name -- vc_opts >> (fn args =>
(Toplevel.print o Toplevel.theory_to_proof (boogie_vc args))))
@@ -329,7 +329,7 @@
val _ =
Outer_Syntax.improper_command "boogie_status"
- "Show the name and state of all loaded verification conditions."
+ "show the name and state of all loaded verification conditions"
Keyword.diag
(status_test >> status_cmd ||
status_vc >> status_cmd ||
@@ -338,7 +338,7 @@
val _ =
Outer_Syntax.command "boogie_end"
- "Close the current Boogie environment."
+ "close the current Boogie environment"
Keyword.thy_decl
(Scan.succeed (Toplevel.theory boogie_end))
--- a/src/HOL/Tools/Quotient/quotient_info.ML Fri Jul 23 10:58:13 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_info.ML Fri Jul 23 18:42:46 2010 +0200
@@ -282,9 +282,9 @@
Keyword.diag (Scan.succeed (Toplevel.keep (pp_fn o Toplevel.context_of)))
val _ = map improper_command
- [(print_mapsinfo, "print_quotmaps", "prints out all map functions"),
- (print_quotinfo, "print_quotients", "prints out all quotients"),
- (print_qconstinfo, "print_quotconsts", "prints out all quotient constants")]
+ [(print_mapsinfo, "print_quotmaps", "print out all map functions"),
+ (print_quotinfo, "print_quotients", "print out all quotients"),
+ (print_qconstinfo, "print_quotconsts", "print out all quotient constants")]
end; (* structure *)
--- a/src/Pure/Isar/toplevel.ML Fri Jul 23 10:58:13 2010 +0200
+++ b/src/Pure/Isar/toplevel.ML Fri Jul 23 18:42:46 2010 +0200
@@ -632,7 +632,7 @@
fun run_command thy_name tr st =
(case
(case init_of tr of
- SOME name => Exn.capture (fn () => Thy_Load.check_name thy_name name) ()
+ SOME name => Exn.capture (fn () => Thy_Load.consistent_name thy_name name) ()
| NONE => Exn.Result ()) of
Exn.Result () =>
let val int = is_some (init_of tr) in
--- a/src/Pure/ProofGeneral/pgip_isabelle.ML Fri Jul 23 10:58:13 2010 +0200
+++ b/src/Pure/ProofGeneral/pgip_isabelle.ML Fri Jul 23 18:42:46 2010 +0200
@@ -80,7 +80,7 @@
NONE => (NONE, NONE)
| SOME fname =>
let val path = Path.explode fname in
- case Thy_Load.check_file Path.current path of
+ case Thy_Load.test_file Path.current path of
SOME _ => (SOME (PgipTypes.pgipurl_of_path path), NONE)
| NONE => (NONE, SOME fname)
end);
--- a/src/Pure/Thy/html.ML Fri Jul 23 10:58:13 2010 +0200
+++ b/src/Pure/Thy/html.ML Fri Jul 23 18:42:46 2010 +0200
@@ -30,7 +30,7 @@
val theory_source: text -> text
val begin_theory: Url.T * string -> string -> (Url.T option * string) list ->
(Url.T * Url.T * bool) list -> text -> text
- val ml_file: Url.T -> string -> text
+ val external_file: Url.T -> string -> text
end;
structure HTML: HTML =
@@ -309,7 +309,7 @@
begin_document ("Index of " ^ session) ^ up_link up ^
para ("View " ^ href_path graph "theory dependencies" ^
implode (map (fn (p, name) => "<br/>\nView " ^ href_path p name) docs)) ^
- "\n</div>\n<hr/>\n<div class=\"theories\">\n<h2>Theories</h2>\n<ul>\n";
+ "\n</div>\n<div class=\"theories\">\n<h2>Theories</h2>\n<ul>\n";
fun choice chs s = space_implode " " (map (fn (s', lnk) =>
enclose "[" "]" (if s = s' then keyword s' else href_name lnk s')) chs);
@@ -329,12 +329,12 @@
(name, begin_document ("Theory dependencies of " ^ session) ^
back_link back ^
para browser_size ^
- "\n</div>\n<hr/>\n<div class=\"graphbrowser\">\n\
+ "\n</div>\n<div class=\"graphbrowser\">\n\
\<applet code=\"GraphBrowser/GraphBrowser.class\" \
\archive=\"GraphBrowser.jar\" \
\width=" ^ quote width ^ " height=" ^ quote height ^ ">\n\
\<param name=\"graphfile\" value=\"" ^ "session.graph" ^ "\"/>\n\
- \</applet>\n<hr/>" ^ end_document)
+ \</applet>" ^ end_document)
end;
in map applet_page sizes end;
@@ -345,15 +345,15 @@
fun session_entries [] = "</ul>"
| session_entries es =
- "</ul>\n</div>\n<hr/>\n<div class=\"sessions\">\n\
+ "</ul>\n</div>\n<div class=\"sessions\">\n\
\<h2>Sessions</h2>\n<ul>\n" ^ implode (map entry es) ^ "</ul>";
(* theory *)
val theory_source = enclose
- "\n</div>\n<hr/>\n<div class=\"source\">\n<pre>"
- "</pre>\n<hr/>\n";
+ "\n</div>\n<div class=\"source\">\n<pre>"
+ "</pre>\n";
local
@@ -379,13 +379,13 @@
end;
-(* ML file *)
+(* external file *)
-fun ml_file path str =
+fun external_file path str =
begin_document ("File " ^ Url.implode path) ^
- "\n</div>\n<hr/><div class=\"mlsource\">\n" ^
+ "\n</div><div class=\"external_source\">\n" ^
verbatim str ^
- "\n</div>\n<hr/>\n<div class=\"mlfooter\">" ^
+ "\n</div>\n<div class=\"external_footer\">" ^
end_document;
end;
--- a/src/Pure/Thy/present.ML Fri Jul 23 10:58:13 2010 +0200
+++ b/src/Pure/Thy/present.ML Fri Jul 23 18:42:46 2010 +0200
@@ -460,18 +460,14 @@
val parents = Theory.parents_of thy;
val parent_specs = map (parent_link remote_path path) parents;
- fun prep_file (raw_path, loadit) =
- (case Thy_Load.check_ml dir raw_path of
- SOME (path, _) =>
- let
- val base = Path.base path;
- val base_html = html_ext base;
- val _ = add_file (Path.append html_prefix base_html,
- HTML.ml_file (Url.File base) (File.read path));
- in (Url.File base_html, Url.File raw_path, loadit) end
- | NONE => error ("Browser info: expected to find ML file " ^ quote (Path.implode raw_path)));
-
- val files_html = map prep_file files;
+ val files_html = files |> map (fn (raw_path, loadit) =>
+ let
+ val path = #1 (Thy_Load.check_file dir raw_path);
+ val base = Path.base path;
+ val base_html = html_ext base;
+ val _ = add_file (Path.append html_prefix base_html,
+ HTML.external_file (Url.File base) (File.read path));
+ in (Url.File base_html, Url.File raw_path, loadit) end);
fun prep_html_source (tex_source, html_source, html) =
let
--- a/src/Pure/Thy/thy_info.ML Fri Jul 23 10:58:13 2010 +0200
+++ b/src/Pure/Thy/thy_info.ML Fri Jul 23 18:42:46 2010 +0200
@@ -8,7 +8,6 @@
signature THY_INFO =
sig
datatype action = Update | Outdate | Remove
- val str_of_action: action -> string
val add_hook: (action -> string -> unit) -> unit
val get_names: unit -> string list
val known_thy: string -> bool
@@ -19,7 +18,6 @@
val is_finished: string -> bool
val master_directory: string -> Path.T
val loaded_files: string -> Path.T list
- val get_parents: string -> string list
val touch_thy: string -> unit
val touch_child_thys: string -> unit
val thy_ord: theory * theory -> order
@@ -44,7 +42,6 @@
(** theory loader actions and hooks **)
datatype action = Update | Outdate | Remove;
-val str_of_action = fn Update => "Update" | Outdate => "Outdate" | Remove => "Remove";
local
val hooks = Unsynchronized.ref ([]: (action -> string -> unit) list);
@@ -296,11 +293,7 @@
let
val dir = master_directory name;
val _ = check_unfinished error name;
- in
- (case Thy_Load.check_file dir path of
- SOME path_info => change_deps name (provide path name path_info)
- | NONE => error ("Could not find file " ^ quote (Path.implode path)))
- end;
+ in change_deps name (provide path name (Thy_Load.check_file dir path)) end;
fun load_file path =
if ! Output.timing then
@@ -417,12 +410,12 @@
local
-fun check_ml master (src_path, info) =
+fun check_file master (src_path, info) =
let val info' =
(case info of
NONE => NONE
| SOME (_, id) =>
- (case Thy_Load.check_ml (master_dir master) src_path of
+ (case Thy_Load.test_file (master_dir master) src_path of
NONE => NONE
| SOME (path', id') => if id <> id' then NONE else SOME (path', id')))
in (src_path, info') end;
@@ -444,7 +437,7 @@
in (false, init_deps master' text' parents' files', parents') end
else
let
- val files' = map (check_ml master') files;
+ val files' = map (check_file master') files;
val current = update_time >= 0 andalso can get_theory name
andalso forall (is_some o snd) files';
val update_time' = if current then update_time else ~1;
--- a/src/Pure/Thy/thy_load.ML Fri Jul 23 10:58:13 2010 +0200
+++ b/src/Pure/Thy/thy_load.ML Fri Jul 23 18:42:46 2010 +0200
@@ -1,7 +1,8 @@
(* Title: Pure/Thy/thy_load.ML
Author: Markus Wenzel, TU Muenchen
-Theory loader primitives, including load path.
+Loading files that contribute to a theory, including global load path
+management.
*)
signature BASIC_THY_LOAD =
@@ -10,22 +11,19 @@
val add_path: string -> unit
val path_add: string -> unit
val del_path: string -> unit
- val with_path: string -> ('a -> 'b) -> 'a -> 'b
- val with_paths: string list -> ('a -> 'b) -> 'a -> 'b
val reset_path: unit -> unit
end;
signature THY_LOAD =
sig
include BASIC_THY_LOAD
- val ml_exts: string list
val ml_path: string -> Path.T
val thy_path: string -> Path.T
val split_thy_path: Path.T -> Path.T * string
- val check_file: Path.T -> Path.T -> (Path.T * File.ident) option
- val check_ml: Path.T -> Path.T -> (Path.T * File.ident) option
+ val consistent_name: string -> string -> unit
+ val test_file: Path.T -> Path.T -> (Path.T * File.ident) option
+ val check_file: Path.T -> Path.T -> Path.T * File.ident
val check_thy: Path.T -> string -> Path.T * File.ident
- val check_name: string -> string -> unit
val deps_thy: Path.T -> string ->
{master: Path.T * File.ident, text: string, imports: string list, uses: Path.T list}
val load_ml: Path.T -> Path.T -> Path.T * File.ident
@@ -50,13 +48,7 @@
CRITICAL (fn () =>
(del_path s; Unsynchronized.change load_path (fn path => path @ [Path.explode s])));
-fun reset_path () = load_path := [Path.current];
-
-fun with_paths ss f x =
- CRITICAL (fn () =>
- setmp_CRITICAL load_path (! load_path @ map Path.explode ss) f x);
-
-fun with_path s f x = with_paths [s] f x;
+fun reset_path () = CRITICAL (fn () => load_path := [Path.current]);
fun search_path dir path =
distinct (op =) (dir :: (if Path.is_basic path then (! load_path) else [Path.current]));
@@ -66,7 +58,6 @@
(* file formats *)
-val ml_exts = ["ML", "sml"];
val ml_path = Path.ext "ML" o Path.basic;
val thy_path = Path.ext "thy" o Path.basic;
@@ -75,38 +66,46 @@
(path', "thy") => (Path.dir path', Path.implode (Path.base path'))
| _ => error ("Bad theory file specification " ^ Path.implode path));
+fun consistent_name name name' =
+ if name = name' then ()
+ else error ("Filename " ^ quote (Path.implode (thy_path name)) ^
+ " does not agree with theory name " ^ quote name');
+
(* check files *)
-fun check_ext exts paths src_path =
+local
+
+exception NOT_FOUND of Path.T list * Path.T;
+
+fun try_file dir src_path =
let
+ val prfxs = search_path dir src_path;
val path = Path.expand src_path;
val _ = Path.is_current path andalso error "Bad file specification";
-
- fun try_ext rel_path ext =
- let val ext_path = Path.expand (Path.ext ext rel_path)
- in Option.map (fn id => (File.full_path ext_path, id)) (File.ident ext_path) end;
- fun try_prfx prfx = get_first (try_ext (Path.append prfx path)) ("" :: exts);
- in get_first try_prfx paths end;
-
-fun check_file dir path = check_ext [] (search_path dir path) path;
-fun check_ml dir path = check_ext ml_exts (search_path dir path) path;
-
-fun check_thy dir name =
- let
- val thy_file = thy_path name;
- val paths = search_path dir thy_file;
+ val result =
+ prfxs |> get_first (fn prfx =>
+ let val full_path = File.full_path (Path.append prfx path)
+ in Option.map (pair full_path) (File.ident full_path) end);
in
- (case check_ext [] paths thy_file of
- NONE => error ("Could not find theory file " ^ quote (Path.implode thy_file) ^
- " in " ^ commas_quote (map Path.implode paths))
- | SOME thy_id => thy_id)
+ (case result of
+ SOME res => res
+ | NONE => raise NOT_FOUND (prfxs, path))
end;
-fun check_name name name' =
- if name = name' then ()
- else error ("Filename " ^ quote (Path.implode (thy_path name)) ^
- " does not agree with theory name " ^ quote name');
+in
+
+fun test_file dir file =
+ SOME (try_file dir file) handle NOT_FOUND _ => NONE;
+
+fun check_file dir file =
+ try_file dir file handle NOT_FOUND (prfxs, path) =>
+ error ("Could not find file " ^ quote (Path.implode path) ^
+ "\nin " ^ commas_quote (map Path.implode prfxs));
+
+fun check_thy dir name = check_file dir (thy_path name);
+
+end;
(* theory deps *)
@@ -117,17 +116,18 @@
val text = File.read path;
val (name', imports, uses) =
Thy_Header.read (Path.position path) (Source.of_string_limited 8000 text);
- val _ = check_name name name';
+ val _ = consistent_name name name';
val uses = map (Path.explode o #1) uses;
in {master = master, text = text, imports = imports, uses = uses} end;
-(* load files *)
+(* ML files *)
fun load_ml dir raw_path =
- (case check_ml dir raw_path of
- NONE => error ("Could not find ML file " ^ quote (Path.implode raw_path))
- | SOME (path, id) => (ML_Context.eval_file path; (path, id)));
+ let
+ val (path, id) = check_file dir raw_path;
+ val _ = ML_Context.eval_file path;
+ in (path, id) end;
end;
--- a/src/Pure/codegen.ML Fri Jul 23 10:58:13 2010 +0200
+++ b/src/Pure/codegen.ML Fri Jul 23 18:42:46 2010 +0200
@@ -1019,12 +1019,12 @@
val _ =
Outer_Syntax.command "code_library"
- "generates code for terms (one structure for each theory)" Keyword.thy_decl
+ "generate code for terms (one structure for each theory)" Keyword.thy_decl
(parse_code true);
val _ =
Outer_Syntax.command "code_module"
- "generates code for terms (single structure, incremental)" Keyword.thy_decl
+ "generate code for terms (single structure, incremental)" Keyword.thy_decl
(parse_code false);
end;