removed all_sessions.graph;
authorwenzelm
Sun Jul 23 12:10:11 2000 +0200 (2000-07-23)
changeset 94169144976964e7
parent 9415 daa2296f23ea
child 9417 c4f7c959eaee
removed all_sessions.graph;
improved graph 'directories';
tuned;
src/Pure/Thy/present.ML
     1.1 --- a/src/Pure/Thy/present.ML	Sun Jul 23 12:08:54 2000 +0200
     1.2 +++ b/src/Pure/Thy/present.ML	Sun Jul 23 12:10:11 2000 +0200
     1.3 @@ -1,9 +1,9 @@
     1.4  (*  Title:      Pure/Thy/present.ML
     1.5      ID:         $Id$
     1.6 -    Author:     Stefan Berghofer and Markus Wenzel, TU Muenchen
     1.7 +    Author:     Markus Wenzel and Stefan Berghofer, TU Muenchen
     1.8      License:    GPL (GNU GENERAL PUBLIC LICENSE)
     1.9  
    1.10 -Theory presentation (HTML, graph files, (PDF)LaTeX documents).
    1.11 +Theory presentation: HTML, graph files, (PDF)LaTeX documents.
    1.12  *)
    1.13  
    1.14  signature BASIC_PRESENT =
    1.15 @@ -29,7 +29,7 @@
    1.16    val subsection: string -> unit
    1.17    val subsubsection: string -> unit
    1.18    val setup: (theory -> theory) list
    1.19 -  val get_info: theory -> {session: string list, is_local: bool}
    1.20 +  val get_info: theory -> {name: string, session: string list, is_local: bool}
    1.21  end;
    1.22  
    1.23  structure Present: PRESENT =
    1.24 @@ -55,7 +55,7 @@
    1.25  
    1.26  fun mk_rel_path [] ys = Path.make ys
    1.27    | mk_rel_path xs [] = Path.appends (replicate (length xs) Path.parent)
    1.28 -  | mk_rel_path (ps as x::xs) (qs as y::ys) = if x=y then mk_rel_path xs ys else
    1.29 +  | mk_rel_path (ps as x :: xs) (qs as y :: ys) = if x = y then mk_rel_path xs ys else
    1.30        Path.appends (replicate (length ps) Path.parent @ [Path.make qs]);
    1.31  
    1.32  
    1.33 @@ -64,9 +64,9 @@
    1.34  structure BrowserInfoArgs =
    1.35  struct
    1.36    val name = "Pure/browser_info";
    1.37 -  type T = {session: string list, is_local: bool};
    1.38 +  type T = {name: string, session: string list, is_local: bool};
    1.39  
    1.40 -  val empty = {session = [], is_local = false};
    1.41 +  val empty = {name = "Pure", session = [], is_local = false};
    1.42    val copy = I;
    1.43    fun prep_ext _ = empty;
    1.44    fun merge _ = empty;
    1.45 @@ -87,44 +87,32 @@
    1.46    {name: string, ID: string, dir: string, unfold: bool,
    1.47     path: string, parents: string list};
    1.48  
    1.49 -fun get_graph path = map (fn (a :: b :: c :: d :: e :: r) =>
    1.50 -  {name = unenclose a, ID = unenclose b,
    1.51 -   dir = unenclose c, unfold = (d = "+"),
    1.52 -   path = unenclose (if d = "+" then e else d),
    1.53 -   parents = map unenclose (fst (split_last (if d = "+" then tl r else r)))})
    1.54 -     (map (filter_out (equal "") o space_explode " ") (split_lines (File.read path)));
    1.55 +fun write_graph gr path =
    1.56 +  File.write path (cat_lines (map (fn {name, ID, dir, unfold, path, parents} =>
    1.57 +    "\"" ^ name ^ "\" \"" ^ ID ^ "\" \"" ^ dir ^ (if unfold then "\" + \"" else "\" \"") ^
    1.58 +    path ^ "\" > " ^ space_implode " " (map quote parents) ^ " ;") gr));
    1.59  
    1.60 -fun put_graph gr path =
    1.61 -    File.write path (cat_lines (map (fn {name, ID, dir, unfold, path, parents} =>
    1.62 -      "\"" ^ name ^ "\" \"" ^ ID ^ "\" \"" ^ dir ^ (if unfold then "\" + \"" else "\" \"") ^
    1.63 -      path ^ "\" > " ^ space_implode " " (map quote parents) ^ " ;") gr));
    1.64 -
    1.65 -fun dir_of sess = space_implode "/" (case sess of
    1.66 -  [] => ["Pure"] | [x] => [x, "base"] | xs => xs);
    1.67 -
    1.68 -fun ID_of sess s = dir_of sess ^ "/" ^ s;
    1.69 -
    1.70 +fun ID_of sess s = space_implode "/" (sess @ [s]);
    1.71  
    1.72 -(* retrieve graph data from theory loader database *)
    1.73 -
    1.74 -fun make_graph remote_path unfold curr_sess = map (fn name =>
    1.75 +(*retrieve graph data from initial theory loader database*)
    1.76 +fun init_graph remote_path curr_sess = map (fn name =>
    1.77    let
    1.78 -    val {session, is_local} = get_info (ThyInfo.theory name);
    1.79 -    val path' = Path.append (Path.make session) (html_path name)
    1.80 +    val {name = sess_name, session, is_local} = get_info (ThyInfo.theory name);
    1.81 +    val path' = Path.append (Path.make session) (html_path name);
    1.82    in
    1.83 -    {name = name, ID = ID_of session name, dir = dir_of session,
    1.84 -     path = if null session then "" else
    1.85 -            if is_some remote_path andalso not is_local then
    1.86 -              Url.pack (Url.append (the remote_path) (Url.file
    1.87 -                (Path.append (Path.make session) (html_path name))))
    1.88 -            else Path.pack (Path.append
    1.89 -              (mk_rel_path curr_sess session) (html_path name)),
    1.90 -     unfold = unfold andalso (length session = 1),
    1.91 -     parents = map (fn s => ID_of (#session (get_info (ThyInfo.theory s))) s)
    1.92 -       (ThyInfo.get_preds name)}
    1.93 +   {name = name, ID = ID_of session name, dir = sess_name,
    1.94 +    path =
    1.95 +      if null session then "" else
    1.96 +      if is_some remote_path andalso not is_local then
    1.97 +        Url.pack (Url.append (the remote_path) (Url.file
    1.98 +          (Path.append (Path.make session) (html_path name))))
    1.99 +      else Path.pack (Path.append (mk_rel_path curr_sess session) (html_path name)),
   1.100 +    unfold = false,
   1.101 +    parents =
   1.102 +      map (fn s => ID_of (#session (get_info (ThyInfo.theory s))) s) (ThyInfo.get_preds name)}
   1.103    end) (ThyInfo.names ());
   1.104  
   1.105 -fun add_graph_entry' (entry as {ID, ...}) (gr : graph_node list) =
   1.106 +fun ins_graph_entry (entry as {ID, ...}) (gr: graph_node list) =
   1.107    filter_out (fn entry' => #ID entry' = ID) gr @ [entry];
   1.108  
   1.109  
   1.110 @@ -147,20 +135,19 @@
   1.111  (* type browser_info *)
   1.112  
   1.113  type browser_info = {theories: theory_info Symtab.table, tex_index: Buffer.T,
   1.114 -  html_index: Buffer.T, graph: graph_node list, all_graph: graph_node list};
   1.115 +  html_index: Buffer.T, graph: graph_node list};
   1.116  
   1.117 -fun make_browser_info (theories, tex_index, html_index, graph, all_graph) =
   1.118 +fun make_browser_info (theories, tex_index, html_index, graph) =
   1.119    {theories = theories, tex_index = tex_index, html_index = html_index,
   1.120 -    graph = graph, all_graph = all_graph}: browser_info;
   1.121 +    graph = graph}: browser_info;
   1.122  
   1.123 -val empty_browser_info = make_browser_info (Symtab.empty, Buffer.empty, Buffer.empty, [], []);
   1.124 +val empty_browser_info = make_browser_info (Symtab.empty, Buffer.empty, Buffer.empty, []);
   1.125  
   1.126 -fun initial_browser_info remote_path graph_path curr_sess = make_browser_info
   1.127 -  (Symtab.empty, Buffer.empty, Buffer.empty, make_graph remote_path false curr_sess,
   1.128 -   if_none (try get_graph graph_path) (make_graph remote_path true [hd curr_sess]));
   1.129 +fun init_browser_info remote_path curr_sess = make_browser_info
   1.130 +  (Symtab.empty, Buffer.empty, Buffer.empty, init_graph remote_path curr_sess);
   1.131  
   1.132 -fun map_browser_info f {theories, tex_index, html_index, graph, all_graph} =
   1.133 -  make_browser_info (f (theories, tex_index, html_index, graph, all_graph));
   1.134 +fun map_browser_info f {theories, tex_index, html_index, graph} =
   1.135 +  make_browser_info (f (theories, tex_index, html_index, graph));
   1.136  
   1.137  
   1.138  (* state *)
   1.139 @@ -170,34 +157,28 @@
   1.140  fun change_browser_info f = browser_info := map_browser_info f (! browser_info);
   1.141  
   1.142  fun init_theory_info name info =
   1.143 -  change_browser_info (fn (theories, tex_index, html_index, graph, all_graph) =>
   1.144 -    (Symtab.update ((name, info), theories), tex_index, html_index, graph, all_graph));
   1.145 +  change_browser_info (fn (theories, tex_index, html_index, graph) =>
   1.146 +    (Symtab.update ((name, info), theories), tex_index, html_index, graph));
   1.147  
   1.148  fun change_theory_info name f =
   1.149 -  change_browser_info (fn (info as (theories, tex_index, html_index, graph, all_graph)) =>
   1.150 +  change_browser_info (fn (info as (theories, tex_index, html_index, graph)) =>
   1.151      (case Symtab.lookup (theories, name) of
   1.152        None => (warning ("Browser info: cannot access theory document " ^ quote name); info)
   1.153      | Some info => (Symtab.update ((name, map_theory_info f info), theories),
   1.154 -        tex_index, html_index, graph, all_graph)));
   1.155 +        tex_index, html_index, graph)));
   1.156  
   1.157  
   1.158  fun add_tex_index txt =
   1.159 -  change_browser_info (fn (theories, tex_index, html_index, graph, all_graph) =>
   1.160 -    (theories, Buffer.add txt tex_index, html_index, graph, all_graph));
   1.161 +  change_browser_info (fn (theories, tex_index, html_index, graph) =>
   1.162 +    (theories, Buffer.add txt tex_index, html_index, graph));
   1.163  
   1.164  fun add_html_index txt =
   1.165 -  change_browser_info (fn (theories, tex_index, html_index, graph, all_graph) =>
   1.166 -    (theories, tex_index, Buffer.add txt html_index, graph, all_graph));
   1.167 +  change_browser_info (fn (theories, tex_index, html_index, graph) =>
   1.168 +    (theories, tex_index, Buffer.add txt html_index, graph));
   1.169  
   1.170 -(*add entry to graph for current session*)
   1.171  fun add_graph_entry e =
   1.172 -  change_browser_info (fn (theories, tex_index, html_index, graph, all_graph) =>
   1.173 -    (theories, tex_index, html_index, add_graph_entry' e graph, all_graph));
   1.174 -
   1.175 -(*add entry to graph for all sessions*)
   1.176 -fun add_all_graph_entry e =
   1.177 -  change_browser_info (fn (theories, tex_index, html_index, graph, all_graph) =>
   1.178 -    (theories, tex_index, html_index, graph, add_graph_entry' e all_graph));
   1.179 +  change_browser_info (fn (theories, tex_index, html_index, graph) =>
   1.180 +    (theories, tex_index, html_index, ins_graph_entry e graph));
   1.181  
   1.182  fun add_tex_source name txt = change_theory_info name (fn (tex_source, html_source, html) =>
   1.183    (Buffer.add txt tex_source, html_source, html));
   1.184 @@ -216,14 +197,12 @@
   1.185  
   1.186  type session_info =
   1.187    {name: string, parent: string, session: string, path: string list, html_prefix: Path.T,
   1.188 -    doc_format: string, doc_prefixes: (Path.T * Path.T option) option,
   1.189 -    all_graph_path: Path.T, remote_path: Url.T option};
   1.190 +    doc_format: string, doc_prefixes: (Path.T * Path.T option) option, remote_path: Url.T option};
   1.191  
   1.192 -fun make_session_info (name, parent, session, path, html_prefix, doc_format, doc_prefixes,
   1.193 -    all_graph_path, remote_path) =
   1.194 +fun make_session_info
   1.195 +    (name, parent, session, path, html_prefix, doc_format, doc_prefixes, remote_path) =
   1.196    {name = name, parent = parent, session = session, path = path, html_prefix = html_prefix,
   1.197 -    doc_format = doc_format, doc_prefixes = doc_prefixes,
   1.198 -    all_graph_path = all_graph_path, remote_path = remote_path}: session_info;
   1.199 +    doc_format = doc_format, doc_prefixes = doc_prefixes, remote_path = remote_path}: session_info;
   1.200  
   1.201  
   1.202  (* state *)
   1.203 @@ -274,10 +253,11 @@
   1.204     File.system_command
   1.205       ("cp " ^ File.sysify_path path1 ^ " " ^ File.sysify_path path2));
   1.206  
   1.207 +
   1.208  fun init false _ _ _ _ _ = (browser_info := empty_browser_info; session_info := None)
   1.209    | init true doc path name dump_path (remote_path, first_time) =
   1.210        let
   1.211 -        val parent_name = name_of_session (take (length path - 1, path));
   1.212 +        val parent_name = name_of_session (Library.take (length path - 1, path));
   1.213          val session_name = name_of_session path;
   1.214          val sess_prefix = Path.make path;
   1.215  
   1.216 @@ -289,8 +269,6 @@
   1.217            else (Some (Path.append html_prefix doc_path, dump_path), Some (Path.ext doc doc_path));
   1.218  
   1.219          val graph_up_lnk = (Url.file index_path, session_name);
   1.220 -        val all_graph_path = Path.appends [out_path,
   1.221 -          Path.basic (hd path), graph_path "all_sessions"];
   1.222  
   1.223          val _ =
   1.224            (copy_files (Path.unpack "~~/lib/browser/awtUtilities/*.class")
   1.225 @@ -319,10 +297,10 @@
   1.226          File.write (Path.append html_prefix session_entries_path) "";
   1.227          if is_some doc_prefixes then File.copy_all doc_path html_prefix else ();
   1.228          seq (fn (name, txt) => File.write (Path.append html_prefix (Path.basic name)) txt)
   1.229 -          (HTML.applet_pages session_name graph_up_lnk (length path = 1));
   1.230 +          (HTML.applet_pages session_name graph_up_lnk);
   1.231          session_info := Some (make_session_info (name, parent_name, session_name, path,
   1.232 -          html_prefix, doc, doc_prefixes, all_graph_path, remote_path));
   1.233 -        browser_info := initial_browser_info remote_path all_graph_path path;
   1.234 +          html_prefix, doc, doc_prefixes, remote_path));
   1.235 +        browser_info := init_browser_info remote_path path;
   1.236          add_html_index index_text
   1.237        end;
   1.238  
   1.239 @@ -346,9 +324,10 @@
   1.240  
   1.241  
   1.242  fun finish () = with_session ()
   1.243 -    (fn {name, html_prefix, doc_format, doc_prefixes, all_graph_path, path, ...} =>
   1.244 +    (fn {name, html_prefix, doc_format, doc_prefixes, path, ...} =>
   1.245    let
   1.246 -    val {theories, tex_index, html_index, graph, all_graph} = ! browser_info;
   1.247 +    val {theories, tex_index, html_index, graph} = ! browser_info;
   1.248 +    val parent_html_prefix = Path.append html_prefix Path.parent;
   1.249  
   1.250      fun finish_node (a, {tex_source, html_source = _, html}) =
   1.251       (doc_prefixes |> apsome (write_texes tex_source a);
   1.252 @@ -358,10 +337,9 @@
   1.253      Buffer.write (Path.append html_prefix pre_index_path) html_index;
   1.254      doc_prefixes |> apsome (write_texes tex_index doc_indexN);
   1.255      doc_prefixes |> apsome (isatool_document doc_format o #1);
   1.256 -    put_graph graph (Path.append html_prefix (graph_path "session"));
   1.257 -    put_graph all_graph all_graph_path;
   1.258 +    write_graph graph (Path.append html_prefix (graph_path "session"));
   1.259      create_index html_prefix;
   1.260 -    if length path > 1 then update_index (Path.append html_prefix Path.parent) name else ();
   1.261 +    if length path > 1 then update_index parent_html_prefix name else ();
   1.262      browser_info := empty_browser_info;
   1.263      session_info := None
   1.264    end);
   1.265 @@ -382,7 +360,7 @@
   1.266  
   1.267  
   1.268  fun parent_link remote_path curr_session name =
   1.269 -  let val {session, is_local} = get_info (ThyInfo.theory name)
   1.270 +  let val {name = _, session, is_local} = get_info (ThyInfo.theory name)
   1.271    in (if null session then None else
   1.272       Some (if is_some remote_path andalso not is_local then
   1.273         Url.append (the remote_path) (Url.file
   1.274 @@ -392,7 +370,7 @@
   1.275    end;
   1.276  
   1.277  fun begin_theory name raw_parents orig_files thy =
   1.278 -  with_session thy (fn {session, path, html_prefix, remote_path, ...} =>
   1.279 +    with_session thy (fn {name = sess_name, session, path, html_prefix, remote_path, ...} =>
   1.280    let
   1.281      val parents = map (parent_link remote_path path) raw_parents;
   1.282      val ml_path = ThyLoad.ml_path name;
   1.283 @@ -421,19 +399,17 @@
   1.284            name parents files_html (Buffer.content html_source)
   1.285        in (tex_source, Buffer.empty, Buffer.add txt html) end;
   1.286  
   1.287 -    fun make_entry unfold all =
   1.288 -      {name = name, ID = ID_of path name, dir = dir_of path, unfold = unfold,
   1.289 -       path = Path.pack (Path.append
   1.290 -         (mk_rel_path (if all then [hd path] else path) path) (html_path name)),
   1.291 -       parents = map (fn s => ID_of (#session (get_info (ThyInfo.theory s))) s) raw_parents};
   1.292 +    val entry =
   1.293 +     {name = name, ID = ID_of path name, dir = sess_name, unfold = true,
   1.294 +      path = Path.pack (html_path name),
   1.295 +      parents = map (fn s => ID_of (#session (get_info (ThyInfo.theory s))) s) raw_parents};
   1.296  
   1.297    in
   1.298      change_theory_info name prep_html_source;
   1.299 -    add_all_graph_entry (make_entry (length path = 1) true);
   1.300 -    add_graph_entry (make_entry true false);
   1.301 +    add_graph_entry entry;
   1.302      add_html_index (HTML.theory_entry (Url.file (html_path name), name));
   1.303      add_tex_index (Latex.theory_entry name);
   1.304 -    BrowserInfoData.put {session = path, is_local = is_some remote_path} thy
   1.305 +    BrowserInfoData.put {name = sess_name, session = path, is_local = is_some remote_path} thy
   1.306    end);
   1.307  
   1.308