src/Pure/Thy/present.ML
changeset 51399 6ac3c29a300e
parent 51398 c3d02b3518c2
child 51400 96361e8f0a54
     1.1 --- a/src/Pure/Thy/present.ML	Mon Mar 11 14:25:14 2013 +0100
     1.2 +++ b/src/Pure/Thy/present.ML	Tue Mar 12 16:47:24 2013 +0100
     1.3 @@ -14,8 +14,8 @@
     1.4    include BASIC_PRESENT
     1.5    val session_name: theory -> string
     1.6    val read_variant: string -> string * string
     1.7 -  val init: bool -> bool -> string -> string -> bool -> string -> (string * string) list ->
     1.8 -    string list -> string -> bool * string -> bool -> theory list -> unit  (*not thread-safe!*)
     1.9 +  val init: bool -> bool -> Path.T -> string -> bool -> string -> (string * string) list ->
    1.10 +    string * string -> bool * string -> bool -> theory list -> unit  (*not thread-safe!*)
    1.11    val finish: unit -> unit  (*not thread-safe!*)
    1.12    val init_theory: string -> unit
    1.13    val theory_source: string -> (unit -> HTML.text) -> unit
    1.14 @@ -44,16 +44,6 @@
    1.15  val graph_pdf_path = Path.basic "session_graph.pdf";
    1.16  val graph_eps_path = Path.basic "session_graph.eps";
    1.17  
    1.18 -val session_path = Path.basic ".session";
    1.19 -val session_entries_path = Path.explode ".session/entries";
    1.20 -val pre_index_path = Path.explode ".session/pre-index";
    1.21 -
    1.22 -fun mk_rel_path [] ys = Path.make ys
    1.23 -  | mk_rel_path xs [] = Path.appends (replicate (length xs) Path.parent)
    1.24 -  | mk_rel_path (ps as x :: xs) (qs as y :: ys) =
    1.25 -      if x = y then mk_rel_path xs ys
    1.26 -      else Path.appends (replicate (length ps) Path.parent @ [Path.make qs]);
    1.27 -
    1.28  fun show_path path = Path.implode (Path.append (File.pwd ()) path);
    1.29  
    1.30  
    1.31 @@ -62,34 +52,41 @@
    1.32  
    1.33  structure Browser_Info = Theory_Data
    1.34  (
    1.35 -  type T = {name: string, session: string list};
    1.36 -  val empty = {name = "", session = []}: T;
    1.37 +  type T = {chapter: string, name: string};
    1.38 +  val empty = {chapter = "Unsorted", name = "Unknown"}: T;  (* FIXME !? *)
    1.39    fun extend _ = empty;
    1.40    fun merge _ = empty;
    1.41  );
    1.42  
    1.43 -val put_info = Browser_Info.put;
    1.44 -val get_info = Browser_Info.get;
    1.45 -val session_name = #name o get_info;
    1.46 +val session_name = #name o Browser_Info.get;
    1.47 +val session_chapter_name = (fn {chapter, name} => [chapter, name]) o Browser_Info.get;
    1.48  
    1.49  
    1.50  
    1.51  (** graphs **)
    1.52  
    1.53  fun ID_of sess s = space_implode "/" (sess @ [s]);
    1.54 -fun ID_of_thy thy = ID_of (#session (get_info thy)) (Context.theory_name thy);
    1.55 +fun ID_of_thy thy = ID_of (session_chapter_name thy) (Context.theory_name thy);
    1.56  
    1.57 +fun theory_link curr_chapter thy =
    1.58 +  let
    1.59 +    val chapter = #chapter (Browser_Info.get thy);
    1.60 +    val thy_html = html_path (Context.theory_name thy);
    1.61 +  in
    1.62 +    if curr_chapter = chapter then thy_html
    1.63 +    else Path.appends [Path.parent, Path.basic chapter, thy_html]
    1.64 +  end;
    1.65  
    1.66  (*retrieve graph data from initial collection of theories*)
    1.67 -fun init_graph curr_sess = rev o map (fn thy =>
    1.68 +fun init_graph curr_chapter = rev o map (fn thy =>
    1.69    let
    1.70 -    val name = Context.theory_name thy;
    1.71 -    val {name = sess_name, session} = get_info thy;
    1.72 +    val {chapter, name = session_name} = Browser_Info.get thy;
    1.73 +    val thy_name = Context.theory_name thy;
    1.74      val entry =
    1.75 -     {name = name, ID = ID_of session name, dir = sess_name,
    1.76 -      path =
    1.77 -        if null session then ""
    1.78 -        else Path.implode (Path.append (mk_rel_path curr_sess session) (html_path name)),
    1.79 +     {name = thy_name,
    1.80 +      ID = ID_of [chapter, session_name] thy_name,
    1.81 +      dir = session_name,
    1.82 +      path = Path.implode (theory_link curr_chapter thy),
    1.83        unfold = false,
    1.84        parents = map ID_of_thy (Theory.parents_of thy),
    1.85        content = []};
    1.86 @@ -127,8 +124,8 @@
    1.87  
    1.88  val empty_browser_info = make_browser_info (Symtab.empty, [], [], [], []);
    1.89  
    1.90 -fun init_browser_info curr_sess thys = make_browser_info
    1.91 -  (Symtab.empty, [], [], [], init_graph curr_sess thys);
    1.92 +fun init_browser_info chapter thys =
    1.93 +  make_browser_info (Symtab.empty, [], [], [], init_graph chapter thys);
    1.94  
    1.95  fun map_browser_info f {theories, files, tex_index, html_index, graph} =
    1.96    make_browser_info (f (theories, files, tex_index, html_index, graph));
    1.97 @@ -186,16 +183,16 @@
    1.98  (* session_info *)
    1.99  
   1.100  type session_info =
   1.101 -  {name: string, parent: string, session: string, path: string list, html_prefix: Path.T,
   1.102 +  {name: string, chapter: string, info_path: Path.T,
   1.103      info: bool, doc_format: string, doc_graph: bool, doc_output: Path.T option,
   1.104      documents: (string * string) list, doc_dump: (bool * string), verbose: bool,
   1.105      readme: Path.T option};
   1.106  
   1.107  fun make_session_info
   1.108 -  (name, parent, session, path, html_prefix, info, doc_format, doc_graph, doc_output,
   1.109 +  (name, chapter, info_path, info, doc_format, doc_graph, doc_output,
   1.110      documents, doc_dump, verbose, readme) =
   1.111 -  {name = name, parent = parent, session = session, path = path, html_prefix = html_prefix,
   1.112 -    info = info, doc_format = doc_format, doc_graph = doc_graph, doc_output = doc_output,
   1.113 +  {name = name, chapter = chapter, info_path = info_path, info = info,
   1.114 +    doc_format = doc_format, doc_graph = doc_graph, doc_output = doc_output,
   1.115      documents = documents, doc_dump = doc_dump, verbose = verbose,
   1.116      readme = readme}: session_info;
   1.117  
   1.118 @@ -204,36 +201,12 @@
   1.119  
   1.120  val session_info = Unsynchronized.ref (NONE: session_info option);
   1.121  
   1.122 -fun session_default x f = (case ! session_info of NONE => x | SOME info => f info);
   1.123 +fun with_session_info x f = (case ! session_info of NONE => x | SOME info => f info);
   1.124  
   1.125  
   1.126  
   1.127  (** document preparation **)
   1.128  
   1.129 -(* maintain session index *)
   1.130 -
   1.131 -val session_entries =
   1.132 -  HTML.session_entries o
   1.133 -    map (fn name => (Url.File (Path.append (Path.basic name) index_path), name));
   1.134 -
   1.135 -fun get_entries dir =
   1.136 -  split_lines (File.read (Path.append dir session_entries_path));
   1.137 -
   1.138 -fun put_entries entries dir =
   1.139 -  File.write (Path.append dir session_entries_path) (cat_lines entries);
   1.140 -
   1.141 -
   1.142 -fun create_index dir =
   1.143 -  File.read (Path.append dir pre_index_path) ^
   1.144 -    session_entries (get_entries dir) ^ HTML.end_document
   1.145 -  |> File.write (Path.append dir index_path);
   1.146 -
   1.147 -fun update_index dir name =
   1.148 -  (case try get_entries dir of
   1.149 -    NONE => warning ("Browser info: cannot access session index of " ^ Path.print dir)
   1.150 -  | SOME es => (put_entries ((remove (op =) name es) @ [name]) dir; create_index dir));
   1.151 -
   1.152 -
   1.153  (* document variants *)
   1.154  
   1.155  fun read_variant str =
   1.156 @@ -245,19 +218,14 @@
   1.157  
   1.158  (* init session *)
   1.159  
   1.160 -fun name_of_session elems = space_implode "/" ("Isabelle" :: elems);
   1.161 -
   1.162 -fun init build info info_path doc doc_graph document_output doc_variants path name
   1.163 -    (doc_dump as (_, dump_prefix)) verbose thys =
   1.164 +fun init build info info_path doc doc_graph document_output doc_variants
   1.165 +    (chapter, name) (doc_dump as (_, dump_prefix)) verbose thys =
   1.166    if not build andalso not info andalso doc = "" andalso dump_prefix = "" then
   1.167      (browser_info := empty_browser_info; session_info := NONE)
   1.168    else
   1.169      let
   1.170 -      val parent_name = name_of_session (take (length path - 1) path);
   1.171 -      val session_name = name_of_session path;
   1.172 -      val sess_prefix = Path.make path;
   1.173 -      val html_prefix = Path.append (Path.expand (Path.explode info_path)) sess_prefix;
   1.174 -      val doc_output = if document_output = "" then NONE else SOME (Path.explode document_output);
   1.175 +      val doc_output =
   1.176 +        if document_output = "" then NONE else SOME (Path.explode document_output);
   1.177  
   1.178        val documents =
   1.179          if doc = "" then []
   1.180 @@ -266,8 +234,6 @@
   1.181             else (); [])
   1.182          else doc_variants;
   1.183  
   1.184 -      val parent_index_path = Path.append Path.parent index_path;
   1.185 -      val index_up_lnk = Url.File parent_index_path;
   1.186        val readme =
   1.187          if File.exists readme_html_path then SOME readme_html_path
   1.188          else if File.exists readme_path then SOME readme_path
   1.189 @@ -276,13 +242,13 @@
   1.190        val docs =
   1.191          (case readme of NONE => [] | SOME p => [(Url.File p, "README")]) @
   1.192            map (fn (name, _) => (Url.File (Path.ext doc (Path.basic name)), name)) documents;
   1.193 -      val index_text = HTML.begin_index (index_up_lnk, parent_name)
   1.194 -        (Url.File index_path, session_name) docs (Url.explode "medium.html");
   1.195 +      val index_text =  (* FIXME move to finish!? *)
   1.196 +        HTML.begin_session_index name docs (Url.explode "medium.html");
   1.197      in
   1.198        session_info :=
   1.199 -        SOME (make_session_info (name, parent_name, session_name, path, html_prefix, info, doc,
   1.200 +        SOME (make_session_info (name, chapter, info_path, info, doc,
   1.201            doc_graph, doc_output, documents, doc_dump, verbose, readme));
   1.202 -      browser_info := init_browser_info path thys;
   1.203 +      browser_info := init_browser_info chapter thys;
   1.204        add_html_index (0, index_text)
   1.205      end;
   1.206  
   1.207 @@ -331,15 +297,18 @@
   1.208  
   1.209  
   1.210  fun finish () =
   1.211 -  session_default () (fn {name, info, html_prefix, doc_format, doc_graph, doc_output,
   1.212 -    documents, doc_dump = (dump_copy, dump_prefix), path, verbose, readme, ...} =>
   1.213 +  with_session_info () (fn {name, chapter, info, info_path, doc_format, doc_graph, doc_output,
   1.214 +    documents, doc_dump = (dump_copy, dump_prefix), verbose, readme, ...} =>
   1.215    let
   1.216      val {theories, files, tex_index, html_index, graph} = ! browser_info;
   1.217      val thys = Symtab.dest theories;
   1.218 -    val parent_html_prefix = Path.append html_prefix Path.parent;
   1.219 +
   1.220 +    val chapter_prefix = Path.append info_path (Path.basic chapter);
   1.221 +    val session_prefix = Path.append chapter_prefix (Path.basic name);
   1.222  
   1.223      fun finish_html (a, {html, ...}: theory_info) =
   1.224 -      File.write_buffer (Path.append html_prefix (html_path a)) (Buffer.add HTML.end_document html);
   1.225 +      File.write_buffer (Path.append session_prefix (html_path a))
   1.226 +        (Buffer.add HTML.end_document html);
   1.227  
   1.228      val sorted_graph = sorted_index graph;
   1.229      val opt_graphs =
   1.230 @@ -349,21 +318,19 @@
   1.231  
   1.232      val _ =
   1.233        if info then
   1.234 -       (Isabelle_System.mkdirs (Path.append html_prefix session_path);
   1.235 -        File.write_buffer (Path.append html_prefix pre_index_path) (index_buffer html_index);
   1.236 -        File.write (Path.append html_prefix session_entries_path) "";
   1.237 -        create_index html_prefix;
   1.238 -        if length path > 1 then update_index parent_html_prefix name else ();
   1.239 -        (case readme of NONE => () | SOME path => File.copy path html_prefix);
   1.240 -        Graph_Display.write_graph_browser (Path.append html_prefix graph_path) sorted_graph;
   1.241 +       (Isabelle_System.mkdirs session_prefix;
   1.242 +        File.write_buffer (Path.append session_prefix index_path)
   1.243 +          (index_buffer html_index |> Buffer.add HTML.end_document);
   1.244 +        (case readme of NONE => () | SOME path => File.copy path session_prefix);
   1.245 +        Graph_Display.write_graph_browser (Path.append session_prefix graph_path) sorted_graph;
   1.246          Isabelle_System.isabelle_tool "browser" "-b";
   1.247 -        File.copy (Path.explode "~~/lib/browser/GraphBrowser.jar") html_prefix;
   1.248 -        List.app (fn (a, txt) => File.write (Path.append html_prefix (Path.basic a)) txt)
   1.249 +        File.copy (Path.explode "~~/lib/browser/GraphBrowser.jar") session_prefix;
   1.250 +        List.app (fn (a, txt) => File.write (Path.append session_prefix (Path.basic a)) txt)
   1.251            (HTML.applet_pages name (Url.File index_path, name));
   1.252 -        File.copy (Path.explode "~~/etc/isabelle.css") html_prefix;
   1.253 +        File.copy (Path.explode "~~/etc/isabelle.css") session_prefix;
   1.254          List.app finish_html thys;
   1.255          List.app (uncurry File.write) files;
   1.256 -        if verbose then Output.physical_stderr ("Browser info at " ^ show_path html_prefix ^ "\n")
   1.257 +        if verbose then Output.physical_stderr ("Browser info at " ^ show_path session_prefix ^ "\n")
   1.258          else ())
   1.259        else ();
   1.260  
   1.261 @@ -409,7 +376,7 @@
   1.262  
   1.263      val jobs =
   1.264        (if info orelse is_none doc_output then
   1.265 -        map (document_job html_prefix true) documents
   1.266 +        map (document_job session_prefix true) documents
   1.267         else []) @
   1.268        (case doc_output of
   1.269          NONE => []
   1.270 @@ -424,30 +391,23 @@
   1.271  
   1.272  (* theory elements *)
   1.273  
   1.274 -fun init_theory name = session_default () (fn _ => init_theory_info name empty_theory_info);
   1.275 +fun init_theory name = with_session_info () (fn _ => init_theory_info name empty_theory_info);
   1.276  
   1.277  fun theory_source name mk_text =
   1.278 -  session_default () (fn _ => add_html_source name (HTML.theory_source (mk_text ())));
   1.279 +  with_session_info () (fn _ => add_html_source name (HTML.theory_source (mk_text ())));
   1.280  
   1.281  fun theory_output name s =
   1.282 -  session_default () (fn _ => add_tex_source name (Latex.isabelle_file name s));
   1.283 +  with_session_info () (fn _ => add_tex_source name (Latex.isabelle_file name s));
   1.284  
   1.285  
   1.286 -fun parent_link curr_session thy =
   1.287 +fun begin_theory update_time dir thy =
   1.288 +    with_session_info thy (fn {name = session_name, chapter, info_path, ...} =>
   1.289    let
   1.290 -    val {name = _, session} = get_info thy;
   1.291 -    val name = Context.theory_name thy;
   1.292 -    val link =
   1.293 -      if null session then NONE
   1.294 -      else SOME (Url.File (Path.append (mk_rel_path curr_session session) (html_path name)));
   1.295 -  in (link, name) end;
   1.296 -
   1.297 -fun begin_theory update_time dir thy =
   1.298 -    session_default thy (fn {name = sess_name, session, path, html_prefix, ...} =>
   1.299 -  let
   1.300 +    val path = [chapter, session_name];
   1.301      val name = Context.theory_name thy;
   1.302      val parents = Theory.parents_of thy;
   1.303 -    val parent_specs = map (parent_link path) parents;
   1.304 +    val parent_specs = parents |> map (fn parent =>
   1.305 +      (SOME (Url.File (theory_link chapter parent)), name));
   1.306  
   1.307      val files = [];  (* FIXME *)
   1.308      val files_html = files |> map (fn (raw_path, loadit) =>
   1.309 @@ -455,18 +415,19 @@
   1.310          val path = File.check_file (File.full_path dir raw_path);
   1.311          val base = Path.base path;
   1.312          val base_html = html_ext base;
   1.313 -        val _ = add_file (Path.append html_prefix base_html,
   1.314 -          HTML.external_file (Url.File base) (File.read path));
   1.315 +        (* FIXME retain file path!? *)
   1.316 +        val session_prefix = Path.appends [info_path, Path.basic chapter, Path.basic name];
   1.317 +        val _ =
   1.318 +          add_file (Path.append session_prefix base_html,
   1.319 +            HTML.external_file (Url.File base) (File.read path));
   1.320        in (Url.File base_html, Url.File raw_path, loadit) end);
   1.321  
   1.322      fun prep_html_source (tex_source, html_source, html) =
   1.323 -      let
   1.324 -        val txt = HTML.begin_theory (Url.File index_path, session)
   1.325 -          name parent_specs files_html (Buffer.content html_source)
   1.326 +      let val txt = HTML.begin_theory name parent_specs files_html (Buffer.content html_source)
   1.327        in (tex_source, Buffer.empty, Buffer.add txt html) end;
   1.328  
   1.329      val entry =
   1.330 -     {name = name, ID = ID_of path name, dir = sess_name, unfold = true,
   1.331 +     {name = name, ID = ID_of path name, dir = session_name, unfold = true,
   1.332        path = Path.implode (html_path name),
   1.333        parents = map ID_of_thy parents,
   1.334        content = []};
   1.335 @@ -475,7 +436,7 @@
   1.336      add_graph_entry (update_time, entry);
   1.337      add_html_index (update_time, HTML.theory_entry (Url.File (html_path name), name));
   1.338      add_tex_index (update_time, Latex.theory_entry name);
   1.339 -    put_info {name = sess_name, session = path} thy
   1.340 +    Browser_Info.put {chapter = chapter, name = session_name} thy
   1.341    end);
   1.342  
   1.343