# HG changeset patch # User wenzelm # Date 1348662213 -7200 # Node ID 7b6aaf446496065e91e6e69734fec3f40761e935 # Parent 6e4510ccf1bb1fc78027ce29187381c8652b6df1 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; diff -r 6e4510ccf1bb -r 7b6aaf446496 src/Pure/Isar/isar_cmd.ML --- 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; diff -r 6e4510ccf1bb -r 7b6aaf446496 src/Pure/Isar/isar_syn.ML --- 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)); diff -r 6e4510ccf1bb -r 7b6aaf446496 src/Pure/Isar/locale.ML --- 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; diff -r 6e4510ccf1bb -r 7b6aaf446496 src/Pure/Pure.thy --- 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 diff -r 6e4510ccf1bb -r 7b6aaf446496 src/Tools/Graphview/lib/Tools/graphview --- 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" diff -r 6e4510ccf1bb -r 7b6aaf446496 src/Tools/Graphview/src/floating_dialog.scala --- 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))) } diff -r 6e4510ccf1bb -r 7b6aaf446496 src/Tools/Graphview/src/graph_panel.scala --- 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 diff -r 6e4510ccf1bb -r 7b6aaf446496 src/Tools/Graphview/src/visualizer.scala --- 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)) + "
" +  // FIXME proper scaling (!?)
+        HTML.encode(txt) + "
" } }