# HG changeset patch
# User wenzelm
# Date 1205879106 -3600
# Node ID 73efc70edeef0a65342be84e6c4552b5c5439684
# Parent  eaf634e975faba8ce0dff7dde81afef7e417bf32
theory loader: discontinued *attached* ML scripts;

diff -r eaf634e975fa -r 73efc70edeef NEWS
--- 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.
 
diff -r eaf634e975fa -r 73efc70edeef src/Pure/Isar/outer_syntax.ML
--- 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;
 
 
 
diff -r eaf634e975fa -r 73efc70edeef src/Pure/Thy/html.ML
--- 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 ^
diff -r eaf634e975fa -r 73efc70edeef src/Pure/Thy/present.ML
--- 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 =