# HG changeset patch
# User wenzelm
# Date 921260891 -3600
# Node ID 3a45ad4a95eb45947e1bdeb61ce1d43ed2a8c806
# Parent  83573ae0f22cac940bcfe157b4bded0dc53e21a7
theory: include parent links;

diff -r 83573ae0f22c -r 3a45ad4a95eb src/Pure/Thy/browser_info.ML
--- a/src/Pure/Thy/browser_info.ML	Thu Mar 11 21:59:26 1999 +0100
+++ b/src/Pure/Thy/browser_info.ML	Fri Mar 12 18:48:11 1999 +0100
@@ -215,8 +215,13 @@
 
 (* FIXME clean *)
 
-fun begin_theory name parents orig_files = with_session (fn {session, html_prefix, ...} =>
+fun parent_link name =
+  if is_some (Symtab.lookup (#theories (! browser_info), name)) then (Some (html_path name), name)
+  else (None, name);
+
+fun begin_theory name raw_parents orig_files = with_session (fn {session, html_prefix, ...} =>
   let
+    val parents = map parent_link raw_parents;
     val ml_path = ThyLoad.ml_path name;
     val files = orig_files @		(* FIXME improve!? *)
       (if is_some (ThyLoad.check_file ml_path) then [(ml_path, true)] else []);
diff -r 83573ae0f22c -r 3a45ad4a95eb src/Pure/Thy/html.ML
--- a/src/Pure/Thy/html.ML	Thu Mar 11 21:59:26 1999 +0100
+++ b/src/Pure/Thy/html.ML	Fri Mar 12 18:48:11 1999 +0100
@@ -27,7 +27,7 @@
   val theory_entry: Path.T * string -> text
   val session_entries: (Path.T * string) list -> text
   val source: (string, 'a) Source.source -> text
-  val begin_theory: Path.T * string -> string -> string list ->
+  val begin_theory: Path.T * string -> string -> (Path.T option * string) list ->
     (Path.T option * Path.T * bool) list -> text -> text
   val end_theory: text
   val ml_file: Path.T -> string -> text
@@ -168,20 +168,23 @@
     (case opt_ref of None => I | Some p => href_path p)
       ((if not loadit then enclose "(" ")" else I) (file_path path));
 
-  fun suffix_last _ [] = []
-    | suffix_last s lst = let val (xs, x) = split_last lst in xs @ [x ^ s] end;
+  fun colon_last [] = []
+    | colon_last lst = let val (prfx, (x, y)) = split_last lst in prfx @ [(x, y ^ ":")] end;
 
-  val plus_names = space_implode " + " o map name;
+  fun parent (None, s) = name s
+    | parent (Some p, s) = href_path p (name s);
+
+  val parents = space_implode " + " o map parent;
 
   fun theory back A =
     begin_document ("Theory " ^ A) ^ "\n" ^ back_link back ^
     keyword "theory" ^ " " ^ name A ^ " = ";
 in
 
-fun begin_theory back A Bs [] body = theory back A ^ plus_names (suffix_last ":" Bs) ^ "\n" ^ body
+fun begin_theory back A Bs [] body = theory back A ^ parents (colon_last Bs) ^ "\n" ^ body
   | begin_theory back A Bs Ps body =
-      theory back A ^ plus_names Bs ^
-      "<br>" ^ keyword "files" ^ " " ^ space_implode " + " (map file Ps) ^ ":" ^ "\n" ^ body;
+      theory back A ^ parents Bs ^ "<br>" ^ keyword "files" ^
+      " " ^ space_implode " + " (map file Ps) ^ ":" ^ "\n" ^ body;
 end;
 
 val end_theory = end_document;