tuned pretty_locale/print_locale, with more basic pretty_locale_deps based on that;
added command 'locale_deps';
graphview prints plain text only -- removed dependency on old Cobra HTML_Panel;

--- a/src/Pure/Isar/isar_cmd.ML	Wed Sep 26 14:13:07 2012 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Wed Sep 26 14:23:33 2012 +0200
@@ -60,8 +60,9 @@
   val print_trans_rules: Toplevel.transition -> Toplevel.transition
   val print_methods: Toplevel.transition -> Toplevel.transition
   val print_antiquotations: Toplevel.transition -> Toplevel.transition
+  val thy_deps: Toplevel.transition -> Toplevel.transition
+  val locale_deps: Toplevel.transition -> Toplevel.transition
   val class_deps: Toplevel.transition -> Toplevel.transition
-  val thy_deps: Toplevel.transition -> Toplevel.transition
   val thm_deps: (Facts.ref * Attrib.src list) list -> Toplevel.transition -> Toplevel.transition
   val unused_thms: (string list * string list option) option ->
     Toplevel.transition -> Toplevel.transition
@@ -409,6 +410,14 @@
       end);
   in Graph_Display.display_graph gr end);
 
+val locale_deps = Toplevel.unknown_theory o Toplevel.keep (fn state =>
+  let
+    val thy = Toplevel.theory_of state;
+    val gr = Locale.pretty_locale_deps thy |> map (fn {name, parents, body} =>
+     {name = Locale.extern thy name, ID = name, parents = parents,
+      dir = "", unfold = true, path = "", content = [body]});
+  in Graph_Display.display_graph gr end);
+
 val class_deps = Toplevel.unknown_theory o Toplevel.keep (fn state =>
   let
     val ctxt = Toplevel.context_of state;

--- a/src/Pure/Isar/isar_syn.ML	Wed Sep 26 14:13:07 2012 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Wed Sep 26 14:23:33 2012 +0200
@@ -858,6 +858,10 @@
     (Scan.succeed (Toplevel.no_timing o Isar_Cmd.thy_deps));
 
 val _ =
+  Outer_Syntax.improper_command @{command_spec "locale_deps"} "visualize locale dependencies"
+    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.locale_deps));
+
+val _ =
   Outer_Syntax.improper_command @{command_spec "class_deps"} "visualize class dependencies"
     (Scan.succeed (Toplevel.no_timing o Isar_Cmd.class_deps));
 

--- a/src/Pure/Isar/locale.ML	Wed Sep 26 14:13:07 2012 +0200
+++ b/src/Pure/Isar/locale.ML	Wed Sep 26 14:23:33 2012 +0200
@@ -76,14 +76,11 @@
     morphism -> theory -> theory
 
   (* Diagnostic *)
-  val all_locales: theory -> string list
   val print_locales: theory -> unit
   val print_locale: theory -> bool -> xstring * Position.T -> unit
   val print_registrations: Proof.context -> xstring * Position.T -> unit
   val print_dependencies: Proof.context -> bool -> morphism -> (string * morphism) list -> unit
-  val locale_deps: theory ->
-    {params: ((string * typ) * mixfix) list, axioms: term list, registrations: term list list} Graph.T
-      * term list list Symtab.table Symtab.table
+  val pretty_locale_deps: theory -> {name: string, parents: string list, body: Pretty.T} list
 end;
 
 structure Locale: LOCALE =
@@ -610,16 +607,13 @@
 
 (*** diagnostic commands and interfaces ***)
 
-val all_locales = Symtab.keys o snd o Locales.get;
-
 fun print_locales thy =
   Pretty.strs ("locales:" ::
     map #1 (Name_Space.extern_table (Proof_Context.init_global thy) (Locales.get thy)))
   |> Pretty.writeln;
 
-fun print_locale thy show_facts raw_name =
+fun pretty_locale thy show_facts name =
   let
-    val name = check thy raw_name;
     val ctxt = init name thy;
     fun cons_elem (elem as Notes _) = show_facts ? cons elem
       | cons_elem elem = cons elem;
@@ -627,10 +621,14 @@
       activate_all name thy cons_elem (K (Element.transfer_morphism thy)) (empty_idents, [])
       |> snd |> rev;
   in
-    Pretty.big_list "locale elements:" (map (Pretty.chunks o Element.pretty_ctxt ctxt) elems)
-    |> Pretty.writeln
+    Pretty.block
+      (Pretty.command "locale" :: Pretty.brk 1 :: Pretty.str (extern thy name) ::
+        maps (fn elem => [Pretty.fbrk, Pretty.chunks (Element.pretty_ctxt ctxt elem)]) elems)
   end;
 
+fun print_locale thy show_facts raw_name =
+  Pretty.writeln (pretty_locale thy show_facts (check thy raw_name));
+
 fun print_registrations ctxt raw_name =
   let
     val thy = Proof_Context.theory_of ctxt;
@@ -651,34 +649,12 @@
     | deps => Pretty.big_list "dependencies:" (map (pretty_reg ctxt) (rev deps)))
   end |> Pretty.writeln;
 
-fun locale_deps thy =
+fun pretty_locale_deps thy =
   let
-    val names = all_locales thy;
-    fun add_locale_node name =
-      let
-        val params = params_of thy name;
-        val axioms =
-          these (Option.map (Logic.strip_imp_prems o Thm.prop_of) (fst (intros_of thy name)));
-        val registrations =
-          map (instance_of thy name o snd) (registrations_of (Context.Theory thy) name);
-      in
-        Graph.new_node (name, {params = params, axioms = axioms, registrations = registrations})
-      end;
-    fun add_locale_deps name =
-      let
-        val dependencies =
-          map (apsnd (instance_of thy name o op $>) o fst) (dependencies_of thy name);
-      in
-        fold (fn (super, ts) => fn (gr, deps) =>
-         (gr |> Graph.add_edge (super, name),
-          deps |> Symtab.map_default (super, Symtab.empty) (Symtab.cons_list (name, ts))))
-            dependencies
-      end;
-  in
-    Graph.empty
-    |> fold add_locale_node names
-    |> rpair Symtab.empty
-    |> fold add_locale_deps names
-  end;
+    fun make_node name =
+     {name = name,
+      parents = map (fst o fst) (dependencies_of thy name),
+      body = pretty_locale thy false name};
+  in map make_node (Symtab.keys (#2 (Locales.get thy))) end;
 
 end;

--- a/src/Pure/Pure.thy	Wed Sep 26 14:13:07 2012 +0200
+++ b/src/Pure/Pure.thy	Wed Sep 26 14:23:33 2012 +0200
@@ -77,7 +77,7 @@
     "print_theorems" "print_locales" "print_classes" "print_locale"
     "print_interps" "print_dependencies" "print_attributes"
     "print_simpset" "print_rules" "print_trans_rules" "print_methods"
-    "print_antiquotations" "thy_deps" "class_deps" "thm_deps"
+    "print_antiquotations" "thy_deps" "locale_deps" "class_deps" "thm_deps"
     "print_binds" "print_facts" "print_cases" "print_statement" "thm"
     "prf" "full_prf" "prop" "term" "typ" "print_codesetup" "unused_thms"
     :: diag

--- a/src/Tools/Graphview/lib/Tools/graphview	Wed Sep 26 14:13:07 2012 +0200
+++ b/src/Tools/Graphview/lib/Tools/graphview	Wed Sep 26 14:23:33 2012 +0200
@@ -21,7 +21,6 @@
   "src/popups.scala"
   "src/shapes.scala"
   "src/visualizer.scala"
-  "../jEdit/src/html_panel.scala"
 )
 
 
@@ -99,8 +98,6 @@
 pushd "$GRAPHVIEW_HOME" >/dev/null || failed
 
 PURE_JAR="$ISABELLE_HOME/lib/classes/ext/Pure.jar"
-COBRA_JAR="$ISABELLE_JEDIT_BUILD_HOME/contrib/cobra.jar"
-JS_JAR="$ISABELLE_JEDIT_BUILD_HOME/contrib/js.jar"
 
 TARGET_DIR="$ISABELLE_HOME/lib/classes"
 TARGET="$TARGET_DIR/ext/Graphview.jar"
@@ -114,9 +111,7 @@
   if [ ! -e "$TARGET" ]; then
     OUTDATED=true
   else
-    if [ -n "$ISABELLE_JEDIT_BUILD_HOME" ]; then
-      declare -a DEPS=("$COBRA_JAR" "$JS_JAR" "$PURE_JAR" "${SOURCES[@]}")
-    elif [ -e "$ISABELLE_HOME/Admin/build" ]; then
+    if [ -e "$ISABELLE_HOME/Admin/build" ]; then
       declare -a DEPS=("$PURE_JAR" "${SOURCES[@]}")
     else
       declare -a DEPS=()
@@ -144,19 +139,10 @@
     done
   }
 
-  [ -z "$ISABELLE_JEDIT_BUILD_HOME" ] && \
-    fail "Unknown ISABELLE_JEDIT_BUILD_HOME -- missing auxiliary component"
-
   rm -rf classes && mkdir classes
 
-  cp -p -R -f "$COBRA_JAR" "$TARGET_DIR/ext" || failed
-  cp -p -R -f "$JS_JAR" "$TARGET_DIR/ext" || failed
-
   (
-    for JAR in "$COBRA_JAR" "$JS_JAR" "$PURE_JAR"
-    do
-      CLASSPATH="$CLASSPATH:$JAR"
-    done
+    CLASSPATH="$CLASSPATH:$PURE_JAR"
     CLASSPATH="$(jvmpath "$CLASSPATH")"
     exec "$SCALA_HOME/bin/scalac" $ISABELLE_SCALA_BUILD_OPTIONS -d classes "${SOURCES[@]}"
   ) || fail "Failed to compile sources"

--- a/src/Tools/Graphview/src/floating_dialog.scala	Wed Sep 26 14:13:07 2012 +0200
+++ b/src/Tools/Graphview/src/floating_dialog.scala	Wed Sep 26 14:23:33 2012 +0200
@@ -8,13 +8,12 @@
 
 
 import isabelle._
-import isabelle.jedit.HTML_Panel
 
-import scala.swing.{Dialog, BorderPanel, Component}
-import java.awt.{Point, Dimension}
+import scala.swing.{Dialog, BorderPanel, Component, TextArea}
+import java.awt.{Font, Point, Dimension}
 
 
-class Floating_Dialog(private val html: String, _title: String, _location: Point)
+class Floating_Dialog(content: XML.Body, _title: String, _location: Point)
 extends Dialog
 {    
   location = _location
@@ -24,20 +23,11 @@
   preferredSize = new Dimension(300, 300)
   peer.setAlwaysOnTop(true)
 
-  private def render_document(text: String) =
-    html_panel.peer.render_document("http://localhost", text)
+  private val text_font = new Font(Parameters.font_family, Font.PLAIN, Parameters.font_size)
+  private val text = new TextArea
+  text.peer.setFont(text_font)
+  text.editable = false
 
-  private val html_panel = new Component()
-  {
-    override lazy val peer: HTML_Panel =
-      new HTML_Panel(Parameters.font_family, Parameters.font_size) with SuperMixin
-      {
-        setPreferredWidth(290)
-      }
-  }
-  
-  render_document(html)
-  contents = new BorderPanel {
-    add(html_panel, BorderPanel.Position.Center)
-  }
+  contents = new BorderPanel { add(text, BorderPanel.Position.Center) }
+  text.text = Pretty.string_of(content, 76, Pretty.font_metric(text.peer.getFontMetrics(text_font)))
 }

--- a/src/Tools/Graphview/src/graph_panel.scala	Wed Sep 26 14:13:07 2012 +0200
+++ b/src/Tools/Graphview/src/graph_panel.scala	Wed Sep 26 14:23:33 2012 +0200
@@ -203,7 +203,7 @@
       def moved(at: Point) {
         val c = Transform.pane_to_graph_coordinates(at)
         node(c) match {
-          case Some(l) => panel.tooltip = vis.Tooltip(l, g.getFontMetrics)
+          case Some(l) => panel.tooltip = vis.Tooltip.text(l, g.getFontMetrics)
           case None => panel.tooltip = null
         }
       }
@@ -260,7 +260,7 @@
                 val p = at.clone.asInstanceOf[Point]
                 SwingUtilities.convertPointToScreen(p, panel.peer)
                 new Floating_Dialog(
-                  vis.Tooltip(l, g.getFontMetrics()),
+                  vis.Tooltip.content(l),
                   vis.Caption(l),
                   at
                 ).open

--- a/src/Tools/Graphview/src/visualizer.scala	Wed Sep 26 14:13:07 2012 +0200
+++ b/src/Tools/Graphview/src/visualizer.scala	Wed Sep 26 14:23:33 2012 +0200
@@ -142,14 +142,14 @@
   }
   
   object Tooltip {
-    import java.awt.FontMetrics
+    def content(name: String): XML.Body = model.complete.get_node(name).content
 
-    def apply(l: String, fm: FontMetrics): String =
+    def text(name: String, fm: java.awt.FontMetrics): String =
     {
-      val info = model.complete.get_node(l)
-      XML.string_of_body(
-        Pretty.formatted(info.content, 76, Pretty.font_metric(fm))
-          .map(t => XML.Elem(Markup(HTML.PRE, Nil), HTML.spans(t, false))))
+      val txt = Pretty.string_of(content(name), 76, Pretty.font_metric(fm))
+      "<html><pre style=\"font-family: " + Parameters.font_family + "; font-size: " +
+          Parameters.font_size + "px; \">" +  // FIXME proper scaling (!?)
+        HTML.encode(txt) + "</pre></html>"
     }
   }