# HG changeset patch
# User wenzelm
# Date 1384629609 -3600
# Node ID 1d977436c1bf051a90bc25c78004a4a6118adf39
# Parent  044faa8a80801881358d722b0de9c73ebdce55b9
removed remains of HTML presentation of auxiliary files -- inactive since Isabelle2013;

diff -r 044faa8a8080 -r 1d977436c1bf src/Pure/Thy/html.ML
--- a/src/Pure/Thy/html.ML	Sat Nov 16 19:23:16 2013 +0100
+++ b/src/Pure/Thy/html.ML	Sat Nov 16 20:20:09 2013 +0100
@@ -12,8 +12,6 @@
   val name: string -> text
   val keyword: string -> text
   val command: string -> text
-  val file_name: string -> text
-  val file_path: Url.T -> text
   val href_name: string -> text -> text
   val href_path: Url.T -> text -> text
   val href_opt_path: Url.T option -> text -> text
@@ -26,9 +24,7 @@
   val applet_pages: string -> Url.T * string -> (string * string) list
   val theory_entry: Url.T * string -> text
   val theory_source: text -> text
-  val begin_theory: string -> (Url.T option * string) list ->
-    (Url.T * Url.T * bool) list -> text -> text
-  val external_file: Url.T -> string -> text
+  val begin_theory: string -> (Url.T option * string) list -> text -> text
 end;
 
 structure HTML: HTML =
@@ -246,8 +242,6 @@
 val name = enclose "<span class=\"name\">" "</span>" o output;
 val keyword = enclose "<span class=\"keyword\">" "</span>" o output;
 val command = enclose "<span class=\"command\">" "</span>" o output;
-val file_name = enclose "<span class=\"filename\">" "</span>" o output;
-val file_path = file_name o Url.implode;
 
 
 (* misc *)
@@ -330,36 +324,9 @@
   "\n</div>\n<div class=\"source\">\n<pre>"
   "</pre>\n";
 
-
-local
-  fun file (href, path, loadit) =
-    href_path href (if loadit then file_path path else enclose "(" ")" (file_path path));
-
-  fun theory A =
-    begin_document ("Theory " ^ A) ^ "\n" ^ command "theory" ^ " " ^ name A;
-
-  fun imports Bs =
-    keyword "imports" ^ " " ^ space_implode " " (map (uncurry href_opt_path o apsnd name) Bs);
-
-  fun uses Ps = keyword "uses" ^ " " ^ space_implode " " (map file Ps) ^ "<br/>\n";
-in
-
-fun begin_theory A Bs Ps body =
-  theory A ^ "<br/>\n" ^
-  imports Bs ^ "<br/>\n" ^
-  (if null Ps then "" else uses Ps) ^
-  body;
+fun begin_theory A Bs body =
+  begin_document ("Theory " ^ A) ^ "\n" ^ command "theory" ^ " " ^ name A ^ "<br/>\n" ^
+  keyword "imports" ^ " " ^ space_implode " " (map (uncurry href_opt_path o apsnd name) Bs) ^
+  "<br/>\n" ^ body;
 
 end;
-
-
-(* external file *)
-
-fun external_file path str =
-  begin_document ("File " ^ Url.implode path) ^
-  "\n</div><div class=\"external_source\">\n" ^
-  verbatim str ^
-  "\n</div>\n<div class=\"external_footer\">" ^
-  end_document;
-
-end;
diff -r 044faa8a8080 -r 1d977436c1bf src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Sat Nov 16 19:23:16 2013 +0100
+++ b/src/Pure/Thy/present.ML	Sat Nov 16 20:20:09 2013 +0100
@@ -15,7 +15,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 -> theory -> theory
+  val begin_theory: int -> theory -> theory
   val display_drafts: Path.T list -> int
 end;
 
@@ -118,21 +118,22 @@
 
 (* type browser_info *)
 
-type browser_info = {theories: theory_info Symtab.table, files: (Path.T * string) list,
-  tex_index: (int * string) list, html_index: (int * string) list,
+type browser_info =
+ {theories: theory_info Symtab.table,
+  tex_index: (int * string) list,
+  html_index: (int * string) list,
   graph: (int * Graph_Display.node) list};
 
-fun make_browser_info (theories, files, tex_index, html_index, graph) =
-  {theories = theories, files = files, tex_index = tex_index, html_index = html_index,
-    graph = graph}: browser_info;
+fun make_browser_info (theories, tex_index, html_index, graph) : browser_info =
+  {theories = theories, tex_index = tex_index, html_index = html_index, graph = graph};
 
-val empty_browser_info = make_browser_info (Symtab.empty, [], [], [], []);
+val empty_browser_info = make_browser_info (Symtab.empty, [], [], []);
 
 fun init_browser_info session thys =
-  make_browser_info (Symtab.empty, [], [], [], init_graph session thys);
+  make_browser_info (Symtab.empty, [], [], init_graph session thys);
 
-fun map_browser_info f {theories, files, tex_index, html_index, graph} =
-  make_browser_info (f (theories, files, tex_index, html_index, graph));
+fun map_browser_info f {theories, tex_index, html_index, graph} =
+  make_browser_info (f (theories, tex_index, html_index, graph));
 
 
 (* state *)
@@ -145,32 +146,28 @@
 fun no_document f x = Unsynchronized.setmp suppress_tex_source true f x;
 
 fun init_theory_info name info =
-  change_browser_info (fn (theories, files, tex_index, html_index, graph) =>
-    (Symtab.update (name, info) theories, files, tex_index, html_index, graph));
+  change_browser_info (fn (theories, tex_index, html_index, graph) =>
+    (Symtab.update (name, info) theories, tex_index, html_index, graph));
 
 fun change_theory_info name f =
-  change_browser_info (fn (theories, files, tex_index, html_index, graph) =>
+  change_browser_info (fn (theories, tex_index, html_index, graph) =>
     (case Symtab.lookup theories name of
       NONE => error ("Browser info: cannot access theory document " ^ quote name)
-    | SOME info => (Symtab.update (name, map_theory_info f info) theories, files,
-        tex_index, html_index, graph)));
+    | SOME info =>
+        (Symtab.update (name, map_theory_info f info) theories, tex_index, html_index, graph)));
 
 
-fun add_file file =
-  change_browser_info (fn (theories, files, tex_index, html_index, graph) =>
-    (theories, file :: files, tex_index, html_index, graph));
-
 fun add_tex_index txt =
-  change_browser_info (fn (theories, files, tex_index, html_index, graph) =>
-    (theories, files, txt :: tex_index, html_index, graph));
+  change_browser_info (fn (theories, tex_index, html_index, graph) =>
+    (theories, txt :: tex_index, html_index, graph));
 
 fun add_html_index txt =
-  change_browser_info (fn (theories, files, tex_index, html_index, graph) =>
-    (theories, files, tex_index, txt :: html_index, graph));
+  change_browser_info (fn (theories, tex_index, html_index, graph) =>
+    (theories, tex_index, txt :: html_index, graph));
 
 fun add_graph_entry entry =
-  change_browser_info (fn (theories, files, tex_index, html_index, graph) =>
-    (theories, files, tex_index, html_index, ins_graph_entry entry graph));
+  change_browser_info (fn (theories, tex_index, html_index, graph) =>
+    (theories, tex_index, html_index, ins_graph_entry entry graph));
 
 fun add_tex_source name txt =
   if ! suppress_tex_source then ()
@@ -299,7 +296,7 @@
   with_session_info () (fn {name, chapter, info, info_path, doc_format, doc_graph, doc_output,
     documents, doc_dump = (dump_copy, dump_prefix), verbose, readme, ...} =>
   let
-    val {theories, files, tex_index, html_index, graph} = ! browser_info;
+    val {theories, tex_index, html_index, graph} = ! browser_info;
     val thys = Symtab.dest theories;
 
     val chapter_prefix = Path.append info_path (Path.basic chapter);
@@ -328,8 +325,8 @@
           (HTML.applet_pages name (Url.File index_path, name));
         File.copy (Path.explode "~~/etc/isabelle.css") session_prefix;
         List.app finish_html thys;
-        List.app (uncurry File.write) files;
-        if verbose then Output.physical_stderr ("Browser info at " ^ show_path session_prefix ^ "\n")
+        if verbose
+        then Output.physical_stderr ("Browser info at " ^ show_path session_prefix ^ "\n")
         else ())
       else ();
 
@@ -398,9 +395,7 @@
 fun theory_output name s =
   with_session_info () (fn _ => add_tex_source name (Latex.isabelle_file name s));
 
-
-fun begin_theory update_time dir thy =
-    with_session_info thy (fn {name = session_name, chapter, info_path, ...} =>
+fun begin_theory update_time thy = with_session_info thy (fn {name = session_name, chapter, ...} =>
   let
     val name = Context.theory_name thy;
     val parents = Theory.parents_of thy;
@@ -408,21 +403,8 @@
       (Option.map Url.File (theory_link (chapter, session_name) parent),
         (Context.theory_name parent)));
 
-    val files = [];  (* FIXME *)
-    val files_html = files |> map (fn (raw_path, loadit) =>
-      let
-        val path = File.check_file (File.full_path dir raw_path);
-        val base = Path.base path;
-        val base_html = html_ext base;
-        (* FIXME retain file path!? *)
-        val session_prefix = Path.appends [info_path, Path.basic chapter, Path.basic name];
-        val _ =
-          add_file (Path.append session_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 val txt = HTML.begin_theory name parent_specs files_html (Buffer.content html_source)
+      let val txt = HTML.begin_theory name parent_specs (Buffer.content html_source)
       in (tex_source, Buffer.empty, Buffer.add txt html) end;
 
     val entry =
diff -r 044faa8a8080 -r 1d977436c1bf src/Pure/Thy/thy_load.ML
--- a/src/Pure/Thy/thy_load.ML	Sat Nov 16 19:23:16 2013 +0100
+++ b/src/Pure/Thy/thy_load.ML	Sat Nov 16 20:20:09 2013 +0100
@@ -171,7 +171,7 @@
     val _ = Present.init_theory name;
     fun init () =
       begin_theory master_dir header parents
-      |> Present.begin_theory update_time master_dir;
+      |> Present.begin_theory update_time;
 
     val lexs = Keyword.get_lexicons ();