# HG changeset patch
# User berghofe
# Date 960372869 -7200
# Node ID 28ee037278a61831dadb35ee9eb32306ee444916
# Parent  ca761fe227d8572d3edd04e04668d063e570a649
Reorganized graph stuff.

diff -r ca761fe227d8 -r 28ee037278a6 src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Wed Jun 07 12:14:18 2000 +0200
+++ b/src/Pure/Thy/present.ML	Wed Jun 07 12:14:29 2000 +0200
@@ -45,9 +45,6 @@
 
 val output_path = Path.variable "ISABELLE_BROWSER_INFO";
 
-fun top_path sess_path offset =
-  Path.append (Path.appends (replicate (offset + length sess_path) Path.parent));
-
 val tex_ext = Path.ext "tex";
 val tex_path = tex_ext o Path.basic;
 val html_ext = Path.ext "html";
@@ -61,6 +58,10 @@
 val session_entries_path = Path.unpack ".session/entries";
 val pre_index_path = Path.unpack ".session/pre-index";
 
+fun mk_rel_path [] ys = Path.make ys
+  | mk_rel_path xs [] = Path.appends (replicate (length xs) Path.parent)
+  | mk_rel_path (ps as x::xs) (qs as y::ys) = if x=y then mk_rel_path xs ys else
+      Path.appends (replicate (length ps) Path.parent @ [Path.make qs]);
 
 
 (** additional theory data **)
@@ -119,8 +120,10 @@
     {name = name, ID = ID_of session name, dir = dir_of session,
      path = if null session then "" else
             if is_some remote_path andalso not is_local then
-              Url.pack (Url.append (the remote_path) (Url.file path'))
-            else Path.pack (top_path curr_sess 2 path'),
+              Url.pack (Url.append (the remote_path) (Url.file
+                (Path.append (Path.make session) (html_path name))))
+            else Path.pack (Path.append
+              (mk_rel_path curr_sess session) (html_path name)),
      unfold = unfold andalso (length session = 1),
      parents = map (fn s => ID_of (#session (get_info (ThyInfo.theory s))) s)
        (ThyInfo.get_preds name)}
@@ -159,7 +162,7 @@
 
 fun initial_browser_info remote_path graph_path curr_sess = make_browser_info
   (Symtab.empty, Buffer.empty, Buffer.empty, make_graph remote_path false curr_sess,
-   if_none (try get_graph graph_path) (make_graph remote_path true [""]));
+   if_none (try get_graph graph_path) (make_graph remote_path true [hd curr_sess]));
 
 fun map_browser_info f {theories, tex_index, html_index, graph, all_graph} =
   make_browser_info (f (theories, tex_index, html_index, graph, all_graph));
@@ -218,13 +221,13 @@
 
 type session_info =
   {name: string, parent: string, session: string, path: string list, html_prefix: Path.T,
-    doc_format: string, doc_prefixes: (Path.T * Path.T option) option, graph_path: Path.T,
+    doc_format: string, doc_prefixes: (Path.T * Path.T option) option,
     all_graph_path: Path.T, remote_path: Url.T option};
 
 fun make_session_info (name, parent, session, path, html_prefix, doc_format, doc_prefixes,
-    graph_path, all_graph_path, remote_path) =
+    all_graph_path, remote_path) =
   {name = name, parent = parent, session = session, path = path, html_prefix = html_prefix,
-    doc_format = doc_format, doc_prefixes = doc_prefixes, graph_path = graph_path,
+    doc_format = doc_format, doc_prefixes = doc_prefixes,
     all_graph_path = all_graph_path, remote_path = remote_path}: session_info;
 
 
@@ -271,6 +274,11 @@
   if File.exists inpath then (File.copy inpath outpath; true)
   else false;
 
+fun copy_files path1 path2 =
+  (File.mkdir path2;
+   File.system_command
+     ("cp " ^ File.sysify_path path1 ^ " " ^ File.sysify_path path2));
+
 fun init false _ _ _ _ _ = (browser_info := empty_browser_info; session_info := None)
   | init true doc path name dump_path (remote_path, first_time) =
       let
@@ -285,17 +293,15 @@
           if doc = "" then (None, None)
           else (Some (Path.append html_prefix doc_path, dump_path), Some (Path.ext doc doc_path));
 
-        val graph_prefix = Path.appends [out_path, Path.unpack "graph/data", sess_prefix];
-        val graph_path = Path.append graph_prefix (Path.basic "session.graph");
-        val graph_lnk = Url.file (top_path path 0 (Path.appends
-          [Path.unpack "graph/data", sess_prefix, Path.basic "medium.html"]));
-        val graph_up_lnk =
-          (Url.file (top_path path 2 (Path.append sess_prefix index_path)), session_name);
-        val codebase = Url.file (top_path path 1 Path.current);
-        val all_graph_path = Path.appends [out_path, Path.unpack "graph/data",
-          Path.basic (hd path), Path.basic "all_sessions.graph"];
+        val graph_up_lnk = (Url.file index_path, session_name);
+        val all_graph_path = Path.appends [out_path,
+          Path.basic (hd path), graph_path "all_sessions"];
 
-        val _ = (File.mkdir html_prefix; File.mkdir graph_prefix);
+        val _ =
+          (copy_files (Path.unpack "~~/lib/browser/awtUtilities/*.class")
+             (Path.append html_prefix (Path.basic "awtUtilities"));
+           copy_files (Path.unpack "~~/lib/browser/GraphBrowser/*.class")
+             (Path.append html_prefix (Path.basic "GraphBrowser")));
 
         fun prep_readme readme =
           let val readme_path = Path.basic readme in
@@ -312,15 +318,15 @@
 
         val index_text = HTML.begin_index (index_up_lnk, parent_name)
           (Url.file index_path, session_name) (apsome Url.file opt_readme)
-            (apsome Url.file document_path) graph_lnk;
+            (apsome Url.file document_path) (Url.unpack "medium.html");
       in
         File.mkdir (Path.append html_prefix session_path);
         File.write (Path.append html_prefix session_entries_path) "";
         if is_some doc_prefixes then File.copy_all doc_path html_prefix else ();
-        seq (fn (name, txt) => File.write (Path.append graph_prefix (Path.basic name)) txt)
-          (HTML.applet_pages session_name codebase graph_up_lnk (length path = 1));
+        seq (fn (name, txt) => File.write (Path.append html_prefix (Path.basic name)) txt)
+          (HTML.applet_pages session_name graph_up_lnk (length path = 1));
         session_info := Some (make_session_info (name, parent_name, session_name, path,
-          html_prefix, doc, doc_prefixes, graph_path, all_graph_path, remote_path));
+          html_prefix, doc, doc_prefixes, all_graph_path, remote_path));
         browser_info := initial_browser_info remote_path all_graph_path path;
         add_html_index index_text
       end;
@@ -345,7 +351,7 @@
 
 
 fun finish () = with_session ()
-    (fn {name, html_prefix, doc_format, doc_prefixes, graph_path, all_graph_path, path, ...} =>
+    (fn {name, html_prefix, doc_format, doc_prefixes, all_graph_path, path, ...} =>
   let
     val {theories, tex_index, html_index, graph, all_graph} = ! browser_info;
 
@@ -357,7 +363,7 @@
     Buffer.write (Path.append html_prefix pre_index_path) html_index;
     doc_prefixes |> apsome (write_texes tex_index doc_indexN);
     doc_prefixes |> apsome (isatool_document doc_format o #1);
-    put_graph graph graph_path;
+    put_graph graph (Path.append html_prefix (graph_path "session"));
     put_graph all_graph all_graph_path;
     create_index html_prefix;
     update_index (Path.append html_prefix Path.parent) name;
@@ -388,13 +394,13 @@
 
 
 fun parent_link remote_path curr_session name =
-  let
-    val {session, is_local} = get_info (ThyInfo.theory name);
-    val path = Path.append (Path.make session) (html_path name)
+  let val {session, is_local} = get_info (ThyInfo.theory name)
   in (if null session then None else
      Some (if is_some remote_path andalso not is_local then
-       Url.append (the remote_path) (Url.file path)
-     else Url.file (top_path curr_session 0 path)), name)
+       Url.append (the remote_path) (Url.file
+         (Path.append (Path.make session) (html_path name)))
+     else Url.file (Path.append (mk_rel_path curr_session session)
+       (html_path name))), name)
   end;
 
 fun begin_theory name raw_parents orig_files thy =
@@ -429,8 +435,8 @@
 
     fun make_entry unfold all =
       {name = name, ID = ID_of path name, dir = dir_of path, unfold = unfold,
-       path = Path.pack (top_path (if all then [""] else path) 2
-         (Path.append (Path.make path) (html_path name))),
+       path = Path.pack (Path.append
+         (mk_rel_path (if all then [hd path] else path) path) (html_path name)),
        parents = map (fn s => ID_of (#session (get_info (ThyInfo.theory s))) s) raw_parents};
 
   in