--- a/NEWS Tue Mar 18 22:19:18 2008 +0100
+++ b/NEWS Tue Mar 18 23:25:06 2008 +0100
@@ -22,6 +22,10 @@
conflict with concurrency. INCOMPATIBILITY, use ML within Isar which
provides a proper context already.
+* Theory loader: old-style ML proof scripts being *attached* to a thy
+file are no longer supported. INCOMPATIBILITY, regular 'uses' and
+'use' within a theory file will do the job.
+
*** Pure ***
@@ -44,7 +48,7 @@
redundant lemmas less_trans, less_linear, le_imp_less_or_eq,
le_less_trans, less_le_trans, which merely duplicate lemmas of the
same name in theory Orderings. Potential INCOMPATIBILITY due to more
-general and different variable names.
+general types and different variable names.
* Library/Option_ord.thy: Canonical order on option type.
--- a/src/Pure/Isar/outer_syntax.ML Tue Mar 18 22:19:18 2008 +0100
+++ b/src/Pure/Isar/outer_syntax.ML Tue Mar 18 23:25:06 2008 +0100
@@ -274,24 +274,11 @@
fun check_text s state = (ThyOutput.eval_antiquote (#1 (get_lexicons ())) state s; ());
-(* load_thy *)
+(* load_thy (backpatching) *)
local
-fun try_ml_file dir name time =
- let val path = ThyLoad.ml_path name in
- if is_none (ThyLoad.check_file dir path) then ()
- else
- let
- val _ = legacy_feature ("Loading attached ML script " ^ quote (Path.implode path));
- val tr = Toplevel.imperative (fn () =>
- ML_Context.setmp (SOME (Context.Theory (ThyInfo.get_theory name)))
- (fn () => ThyInfo.load_file time path) ());
- val tr_name = if time then "time_use" else "use";
- in Toplevel.excursion [Toplevel.empty |> Toplevel.name tr_name |> tr] end
- end;
-
-fun run_thy dir name pos text time =
+fun load_thy dir name pos text time =
let
val text_src = Source.of_list (Library.untabify text);
@@ -313,15 +300,7 @@
val _ = if time then writeln ("**** Finished theory " ^ quote name ^ " ****\n") else ();
in () end;
-fun load_thy dir name pos text time =
- (run_thy dir name pos text time;
- try_ml_file dir name time);
-
-in
-
-val _ = ThyLoad.load_thy_fn := load_thy;
-
-end;
+in val _ = ThyLoad.load_thy_fn := load_thy end;
--- a/src/Pure/Thy/html.ML Tue Mar 18 22:19:18 2008 +0100
+++ b/src/Pure/Thy/html.ML Tue Mar 18 23:25:06 2008 +0100
@@ -32,7 +32,7 @@
val session_entries: (Url.T * string) list -> text
val verbatim_source: Symbol.symbol list -> text
val begin_theory: Url.T * string -> string -> (Url.T option * string) list ->
- (Url.T option * Url.T * bool option) list -> text -> text
+ (Url.T option * Url.T * bool) list -> text -> text
val end_theory: text
val ml_file: Url.T -> string -> text
val results: Proof.context -> string -> (string * thm list) list -> text
@@ -386,11 +386,8 @@
local
- fun encl NONE = enclose "[" "]"
- | encl (SOME false) = enclose "(" ")"
- | encl (SOME true) = I;
-
- fun file (opt_ref, path, loadit) = href_opt_path opt_ref (encl loadit (file_path path));
+ fun file (opt_ref, path, loadit) =
+ href_opt_path opt_ref (if loadit then enclose "(" ")" (file_path path) else file_path path);
fun theory up A =
begin_document ("Theory " ^ A) ^ "\n" ^ up_link up ^
--- a/src/Pure/Thy/present.ML Tue Mar 18 22:19:18 2008 +0100
+++ b/src/Pure/Thy/present.ML Tue Mar 18 23:25:06 2008 +0100
@@ -462,15 +462,12 @@
else Url.File (Path.append (mk_rel_path curr_session session) (html_path name)));
in (link, name) end;
-fun begin_theory update_time dir orig_files thy =
+fun begin_theory update_time dir files thy =
with_session 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 ml_path = ThyLoad.ml_path name;
- val files = map (apsnd SOME) orig_files @
- (if is_some (ThyLoad.check_file dir ml_path) then [(ml_path, NONE)] else []);
fun prep_file (raw_path, loadit) =
(case ThyLoad.check_ml dir raw_path of
@@ -478,21 +475,17 @@
let
val base = Path.base path;
val base_html = html_ext base;
- in
- add_file (Path.append html_prefix base_html,
+ val _ = add_file (Path.append html_prefix base_html,
HTML.ml_file (Url.File base) (File.read path));
- (SOME (Url.File base_html), Url.File raw_path, loadit)
- end
+ in (SOME (Url.File base_html), Url.File raw_path, loadit) end
| NONE =>
(warning ("Browser info: expected to find ML file" ^ quote (Path.implode raw_path));
(NONE, Url.File raw_path, loadit)));
- val files_html = map prep_file files;
-
fun prep_html_source (tex_source, html_source, html) =
let
val txt = HTML.begin_theory (Url.File index_path, session)
- name parent_specs files_html (Buffer.content html_source)
+ name parent_specs (map prep_file files) (Buffer.content html_source)
in (tex_source, Buffer.empty, Buffer.add txt html) end;
val entry =