src/Pure/Thy/present.ML
changeset 54455 1d977436c1bf
parent 53171 a5e54d4d9081
child 54456 f4b1440d9880
     1.1 --- a/src/Pure/Thy/present.ML	Sat Nov 16 19:23:16 2013 +0100
     1.2 +++ b/src/Pure/Thy/present.ML	Sat Nov 16 20:20:09 2013 +0100
     1.3 @@ -15,7 +15,7 @@
     1.4    val init_theory: string -> unit
     1.5    val theory_source: string -> (unit -> HTML.text) -> unit
     1.6    val theory_output: string -> string -> unit
     1.7 -  val begin_theory: int -> Path.T -> theory -> theory
     1.8 +  val begin_theory: int -> theory -> theory
     1.9    val display_drafts: Path.T list -> int
    1.10  end;
    1.11  
    1.12 @@ -118,21 +118,22 @@
    1.13  
    1.14  (* type browser_info *)
    1.15  
    1.16 -type browser_info = {theories: theory_info Symtab.table, files: (Path.T * string) list,
    1.17 -  tex_index: (int * string) list, html_index: (int * string) list,
    1.18 +type browser_info =
    1.19 + {theories: theory_info Symtab.table,
    1.20 +  tex_index: (int * string) list,
    1.21 +  html_index: (int * string) list,
    1.22    graph: (int * Graph_Display.node) list};
    1.23  
    1.24 -fun make_browser_info (theories, files, tex_index, html_index, graph) =
    1.25 -  {theories = theories, files = files, tex_index = tex_index, html_index = html_index,
    1.26 -    graph = graph}: browser_info;
    1.27 +fun make_browser_info (theories, tex_index, html_index, graph) : browser_info =
    1.28 +  {theories = theories, tex_index = tex_index, html_index = html_index, graph = graph};
    1.29  
    1.30 -val empty_browser_info = make_browser_info (Symtab.empty, [], [], [], []);
    1.31 +val empty_browser_info = make_browser_info (Symtab.empty, [], [], []);
    1.32  
    1.33  fun init_browser_info session thys =
    1.34 -  make_browser_info (Symtab.empty, [], [], [], init_graph session thys);
    1.35 +  make_browser_info (Symtab.empty, [], [], init_graph session thys);
    1.36  
    1.37 -fun map_browser_info f {theories, files, tex_index, html_index, graph} =
    1.38 -  make_browser_info (f (theories, files, tex_index, html_index, graph));
    1.39 +fun map_browser_info f {theories, tex_index, html_index, graph} =
    1.40 +  make_browser_info (f (theories, tex_index, html_index, graph));
    1.41  
    1.42  
    1.43  (* state *)
    1.44 @@ -145,32 +146,28 @@
    1.45  fun no_document f x = Unsynchronized.setmp suppress_tex_source true f x;
    1.46  
    1.47  fun init_theory_info name info =
    1.48 -  change_browser_info (fn (theories, files, tex_index, html_index, graph) =>
    1.49 -    (Symtab.update (name, info) theories, files, tex_index, html_index, graph));
    1.50 +  change_browser_info (fn (theories, tex_index, html_index, graph) =>
    1.51 +    (Symtab.update (name, info) theories, tex_index, html_index, graph));
    1.52  
    1.53  fun change_theory_info name f =
    1.54 -  change_browser_info (fn (theories, files, tex_index, html_index, graph) =>
    1.55 +  change_browser_info (fn (theories, tex_index, html_index, graph) =>
    1.56      (case Symtab.lookup theories name of
    1.57        NONE => error ("Browser info: cannot access theory document " ^ quote name)
    1.58 -    | SOME info => (Symtab.update (name, map_theory_info f info) theories, files,
    1.59 -        tex_index, html_index, graph)));
    1.60 +    | SOME info =>
    1.61 +        (Symtab.update (name, map_theory_info f info) theories, tex_index, html_index, graph)));
    1.62  
    1.63  
    1.64 -fun add_file file =
    1.65 -  change_browser_info (fn (theories, files, tex_index, html_index, graph) =>
    1.66 -    (theories, file :: files, tex_index, html_index, graph));
    1.67 -
    1.68  fun add_tex_index txt =
    1.69 -  change_browser_info (fn (theories, files, tex_index, html_index, graph) =>
    1.70 -    (theories, files, txt :: tex_index, html_index, graph));
    1.71 +  change_browser_info (fn (theories, tex_index, html_index, graph) =>
    1.72 +    (theories, txt :: tex_index, html_index, graph));
    1.73  
    1.74  fun add_html_index txt =
    1.75 -  change_browser_info (fn (theories, files, tex_index, html_index, graph) =>
    1.76 -    (theories, files, tex_index, txt :: html_index, graph));
    1.77 +  change_browser_info (fn (theories, tex_index, html_index, graph) =>
    1.78 +    (theories, tex_index, txt :: html_index, graph));
    1.79  
    1.80  fun add_graph_entry entry =
    1.81 -  change_browser_info (fn (theories, files, tex_index, html_index, graph) =>
    1.82 -    (theories, files, tex_index, html_index, ins_graph_entry entry graph));
    1.83 +  change_browser_info (fn (theories, tex_index, html_index, graph) =>
    1.84 +    (theories, tex_index, html_index, ins_graph_entry entry graph));
    1.85  
    1.86  fun add_tex_source name txt =
    1.87    if ! suppress_tex_source then ()
    1.88 @@ -299,7 +296,7 @@
    1.89    with_session_info () (fn {name, chapter, info, info_path, doc_format, doc_graph, doc_output,
    1.90      documents, doc_dump = (dump_copy, dump_prefix), verbose, readme, ...} =>
    1.91    let
    1.92 -    val {theories, files, tex_index, html_index, graph} = ! browser_info;
    1.93 +    val {theories, tex_index, html_index, graph} = ! browser_info;
    1.94      val thys = Symtab.dest theories;
    1.95  
    1.96      val chapter_prefix = Path.append info_path (Path.basic chapter);
    1.97 @@ -328,8 +325,8 @@
    1.98            (HTML.applet_pages name (Url.File index_path, name));
    1.99          File.copy (Path.explode "~~/etc/isabelle.css") session_prefix;
   1.100          List.app finish_html thys;
   1.101 -        List.app (uncurry File.write) files;
   1.102 -        if verbose then Output.physical_stderr ("Browser info at " ^ show_path session_prefix ^ "\n")
   1.103 +        if verbose
   1.104 +        then Output.physical_stderr ("Browser info at " ^ show_path session_prefix ^ "\n")
   1.105          else ())
   1.106        else ();
   1.107  
   1.108 @@ -398,9 +395,7 @@
   1.109  fun theory_output name s =
   1.110    with_session_info () (fn _ => add_tex_source name (Latex.isabelle_file name s));
   1.111  
   1.112 -
   1.113 -fun begin_theory update_time dir thy =
   1.114 -    with_session_info thy (fn {name = session_name, chapter, info_path, ...} =>
   1.115 +fun begin_theory update_time thy = with_session_info thy (fn {name = session_name, chapter, ...} =>
   1.116    let
   1.117      val name = Context.theory_name thy;
   1.118      val parents = Theory.parents_of thy;
   1.119 @@ -408,21 +403,8 @@
   1.120        (Option.map Url.File (theory_link (chapter, session_name) parent),
   1.121          (Context.theory_name parent)));
   1.122  
   1.123 -    val files = [];  (* FIXME *)
   1.124 -    val files_html = files |> map (fn (raw_path, loadit) =>
   1.125 -      let
   1.126 -        val path = File.check_file (File.full_path dir raw_path);
   1.127 -        val base = Path.base path;
   1.128 -        val base_html = html_ext base;
   1.129 -        (* FIXME retain file path!? *)
   1.130 -        val session_prefix = Path.appends [info_path, Path.basic chapter, Path.basic name];
   1.131 -        val _ =
   1.132 -          add_file (Path.append session_prefix base_html,
   1.133 -            HTML.external_file (Url.File base) (File.read path));
   1.134 -      in (Url.File base_html, Url.File raw_path, loadit) end);
   1.135 -
   1.136      fun prep_html_source (tex_source, html_source, html) =
   1.137 -      let val txt = HTML.begin_theory name parent_specs files_html (Buffer.content html_source)
   1.138 +      let val txt = HTML.begin_theory name parent_specs (Buffer.content html_source)
   1.139        in (tex_source, Buffer.empty, Buffer.add txt html) end;
   1.140  
   1.141      val entry =