tuned pretty_locale/print_locale, with more basic pretty_locale_deps based on that;
authorwenzelm
Wed Sep 26 14:23:33 2012 +0200 (2012-09-26 ago)
changeset 495697b6aaf446496
parent 49568 6e4510ccf1bb
child 49570 2265456f6131
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;
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/locale.ML
src/Pure/Pure.thy
src/Tools/Graphview/lib/Tools/graphview
src/Tools/Graphview/src/floating_dialog.scala
src/Tools/Graphview/src/graph_panel.scala
src/Tools/Graphview/src/visualizer.scala
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Wed Sep 26 14:13:07 2012 +0200
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Wed Sep 26 14:23:33 2012 +0200
     1.3 @@ -60,8 +60,9 @@
     1.4    val print_trans_rules: Toplevel.transition -> Toplevel.transition
     1.5    val print_methods: Toplevel.transition -> Toplevel.transition
     1.6    val print_antiquotations: Toplevel.transition -> Toplevel.transition
     1.7 +  val thy_deps: Toplevel.transition -> Toplevel.transition
     1.8 +  val locale_deps: Toplevel.transition -> Toplevel.transition
     1.9    val class_deps: Toplevel.transition -> Toplevel.transition
    1.10 -  val thy_deps: Toplevel.transition -> Toplevel.transition
    1.11    val thm_deps: (Facts.ref * Attrib.src list) list -> Toplevel.transition -> Toplevel.transition
    1.12    val unused_thms: (string list * string list option) option ->
    1.13      Toplevel.transition -> Toplevel.transition
    1.14 @@ -409,6 +410,14 @@
    1.15        end);
    1.16    in Graph_Display.display_graph gr end);
    1.17  
    1.18 +val locale_deps = Toplevel.unknown_theory o Toplevel.keep (fn state =>
    1.19 +  let
    1.20 +    val thy = Toplevel.theory_of state;
    1.21 +    val gr = Locale.pretty_locale_deps thy |> map (fn {name, parents, body} =>
    1.22 +     {name = Locale.extern thy name, ID = name, parents = parents,
    1.23 +      dir = "", unfold = true, path = "", content = [body]});
    1.24 +  in Graph_Display.display_graph gr end);
    1.25 +
    1.26  val class_deps = Toplevel.unknown_theory o Toplevel.keep (fn state =>
    1.27    let
    1.28      val ctxt = Toplevel.context_of state;
     2.1 --- a/src/Pure/Isar/isar_syn.ML	Wed Sep 26 14:13:07 2012 +0200
     2.2 +++ b/src/Pure/Isar/isar_syn.ML	Wed Sep 26 14:23:33 2012 +0200
     2.3 @@ -858,6 +858,10 @@
     2.4      (Scan.succeed (Toplevel.no_timing o Isar_Cmd.thy_deps));
     2.5  
     2.6  val _ =
     2.7 +  Outer_Syntax.improper_command @{command_spec "locale_deps"} "visualize locale dependencies"
     2.8 +    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.locale_deps));
     2.9 +
    2.10 +val _ =
    2.11    Outer_Syntax.improper_command @{command_spec "class_deps"} "visualize class dependencies"
    2.12      (Scan.succeed (Toplevel.no_timing o Isar_Cmd.class_deps));
    2.13  
     3.1 --- a/src/Pure/Isar/locale.ML	Wed Sep 26 14:13:07 2012 +0200
     3.2 +++ b/src/Pure/Isar/locale.ML	Wed Sep 26 14:23:33 2012 +0200
     3.3 @@ -76,14 +76,11 @@
     3.4      morphism -> theory -> theory
     3.5  
     3.6    (* Diagnostic *)
     3.7 -  val all_locales: theory -> string list
     3.8    val print_locales: theory -> unit
     3.9    val print_locale: theory -> bool -> xstring * Position.T -> unit
    3.10    val print_registrations: Proof.context -> xstring * Position.T -> unit
    3.11    val print_dependencies: Proof.context -> bool -> morphism -> (string * morphism) list -> unit
    3.12 -  val locale_deps: theory ->
    3.13 -    {params: ((string * typ) * mixfix) list, axioms: term list, registrations: term list list} Graph.T
    3.14 -      * term list list Symtab.table Symtab.table
    3.15 +  val pretty_locale_deps: theory -> {name: string, parents: string list, body: Pretty.T} list
    3.16  end;
    3.17  
    3.18  structure Locale: LOCALE =
    3.19 @@ -610,16 +607,13 @@
    3.20  
    3.21  (*** diagnostic commands and interfaces ***)
    3.22  
    3.23 -val all_locales = Symtab.keys o snd o Locales.get;
    3.24 -
    3.25  fun print_locales thy =
    3.26    Pretty.strs ("locales:" ::
    3.27      map #1 (Name_Space.extern_table (Proof_Context.init_global thy) (Locales.get thy)))
    3.28    |> Pretty.writeln;
    3.29  
    3.30 -fun print_locale thy show_facts raw_name =
    3.31 +fun pretty_locale thy show_facts name =
    3.32    let
    3.33 -    val name = check thy raw_name;
    3.34      val ctxt = init name thy;
    3.35      fun cons_elem (elem as Notes _) = show_facts ? cons elem
    3.36        | cons_elem elem = cons elem;
    3.37 @@ -627,10 +621,14 @@
    3.38        activate_all name thy cons_elem (K (Element.transfer_morphism thy)) (empty_idents, [])
    3.39        |> snd |> rev;
    3.40    in
    3.41 -    Pretty.big_list "locale elements:" (map (Pretty.chunks o Element.pretty_ctxt ctxt) elems)
    3.42 -    |> Pretty.writeln
    3.43 +    Pretty.block
    3.44 +      (Pretty.command "locale" :: Pretty.brk 1 :: Pretty.str (extern thy name) ::
    3.45 +        maps (fn elem => [Pretty.fbrk, Pretty.chunks (Element.pretty_ctxt ctxt elem)]) elems)
    3.46    end;
    3.47  
    3.48 +fun print_locale thy show_facts raw_name =
    3.49 +  Pretty.writeln (pretty_locale thy show_facts (check thy raw_name));
    3.50 +
    3.51  fun print_registrations ctxt raw_name =
    3.52    let
    3.53      val thy = Proof_Context.theory_of ctxt;
    3.54 @@ -651,34 +649,12 @@
    3.55      | deps => Pretty.big_list "dependencies:" (map (pretty_reg ctxt) (rev deps)))
    3.56    end |> Pretty.writeln;
    3.57  
    3.58 -fun locale_deps thy =
    3.59 +fun pretty_locale_deps thy =
    3.60    let
    3.61 -    val names = all_locales thy;
    3.62 -    fun add_locale_node name =
    3.63 -      let
    3.64 -        val params = params_of thy name;
    3.65 -        val axioms =
    3.66 -          these (Option.map (Logic.strip_imp_prems o Thm.prop_of) (fst (intros_of thy name)));
    3.67 -        val registrations =
    3.68 -          map (instance_of thy name o snd) (registrations_of (Context.Theory thy) name);
    3.69 -      in
    3.70 -        Graph.new_node (name, {params = params, axioms = axioms, registrations = registrations})
    3.71 -      end;
    3.72 -    fun add_locale_deps name =
    3.73 -      let
    3.74 -        val dependencies =
    3.75 -          map (apsnd (instance_of thy name o op $>) o fst) (dependencies_of thy name);
    3.76 -      in
    3.77 -        fold (fn (super, ts) => fn (gr, deps) =>
    3.78 -         (gr |> Graph.add_edge (super, name),
    3.79 -          deps |> Symtab.map_default (super, Symtab.empty) (Symtab.cons_list (name, ts))))
    3.80 -            dependencies
    3.81 -      end;
    3.82 -  in
    3.83 -    Graph.empty
    3.84 -    |> fold add_locale_node names
    3.85 -    |> rpair Symtab.empty
    3.86 -    |> fold add_locale_deps names
    3.87 -  end;
    3.88 +    fun make_node name =
    3.89 +     {name = name,
    3.90 +      parents = map (fst o fst) (dependencies_of thy name),
    3.91 +      body = pretty_locale thy false name};
    3.92 +  in map make_node (Symtab.keys (#2 (Locales.get thy))) end;
    3.93  
    3.94  end;
     4.1 --- a/src/Pure/Pure.thy	Wed Sep 26 14:13:07 2012 +0200
     4.2 +++ b/src/Pure/Pure.thy	Wed Sep 26 14:23:33 2012 +0200
     4.3 @@ -77,7 +77,7 @@
     4.4      "print_theorems" "print_locales" "print_classes" "print_locale"
     4.5      "print_interps" "print_dependencies" "print_attributes"
     4.6      "print_simpset" "print_rules" "print_trans_rules" "print_methods"
     4.7 -    "print_antiquotations" "thy_deps" "class_deps" "thm_deps"
     4.8 +    "print_antiquotations" "thy_deps" "locale_deps" "class_deps" "thm_deps"
     4.9      "print_binds" "print_facts" "print_cases" "print_statement" "thm"
    4.10      "prf" "full_prf" "prop" "term" "typ" "print_codesetup" "unused_thms"
    4.11      :: diag
     5.1 --- a/src/Tools/Graphview/lib/Tools/graphview	Wed Sep 26 14:13:07 2012 +0200
     5.2 +++ b/src/Tools/Graphview/lib/Tools/graphview	Wed Sep 26 14:23:33 2012 +0200
     5.3 @@ -21,7 +21,6 @@
     5.4    "src/popups.scala"
     5.5    "src/shapes.scala"
     5.6    "src/visualizer.scala"
     5.7 -  "../jEdit/src/html_panel.scala"
     5.8  )
     5.9  
    5.10  
    5.11 @@ -99,8 +98,6 @@
    5.12  pushd "$GRAPHVIEW_HOME" >/dev/null || failed
    5.13  
    5.14  PURE_JAR="$ISABELLE_HOME/lib/classes/ext/Pure.jar"
    5.15 -COBRA_JAR="$ISABELLE_JEDIT_BUILD_HOME/contrib/cobra.jar"
    5.16 -JS_JAR="$ISABELLE_JEDIT_BUILD_HOME/contrib/js.jar"
    5.17  
    5.18  TARGET_DIR="$ISABELLE_HOME/lib/classes"
    5.19  TARGET="$TARGET_DIR/ext/Graphview.jar"
    5.20 @@ -114,9 +111,7 @@
    5.21    if [ ! -e "$TARGET" ]; then
    5.22      OUTDATED=true
    5.23    else
    5.24 -    if [ -n "$ISABELLE_JEDIT_BUILD_HOME" ]; then
    5.25 -      declare -a DEPS=("$COBRA_JAR" "$JS_JAR" "$PURE_JAR" "${SOURCES[@]}")
    5.26 -    elif [ -e "$ISABELLE_HOME/Admin/build" ]; then
    5.27 +    if [ -e "$ISABELLE_HOME/Admin/build" ]; then
    5.28        declare -a DEPS=("$PURE_JAR" "${SOURCES[@]}")
    5.29      else
    5.30        declare -a DEPS=()
    5.31 @@ -144,19 +139,10 @@
    5.32      done
    5.33    }
    5.34  
    5.35 -  [ -z "$ISABELLE_JEDIT_BUILD_HOME" ] && \
    5.36 -    fail "Unknown ISABELLE_JEDIT_BUILD_HOME -- missing auxiliary component"
    5.37 -
    5.38    rm -rf classes && mkdir classes
    5.39  
    5.40 -  cp -p -R -f "$COBRA_JAR" "$TARGET_DIR/ext" || failed
    5.41 -  cp -p -R -f "$JS_JAR" "$TARGET_DIR/ext" || failed
    5.42 -
    5.43    (
    5.44 -    for JAR in "$COBRA_JAR" "$JS_JAR" "$PURE_JAR"
    5.45 -    do
    5.46 -      CLASSPATH="$CLASSPATH:$JAR"
    5.47 -    done
    5.48 +    CLASSPATH="$CLASSPATH:$PURE_JAR"
    5.49      CLASSPATH="$(jvmpath "$CLASSPATH")"
    5.50      exec "$SCALA_HOME/bin/scalac" $ISABELLE_SCALA_BUILD_OPTIONS -d classes "${SOURCES[@]}"
    5.51    ) || fail "Failed to compile sources"
     6.1 --- a/src/Tools/Graphview/src/floating_dialog.scala	Wed Sep 26 14:13:07 2012 +0200
     6.2 +++ b/src/Tools/Graphview/src/floating_dialog.scala	Wed Sep 26 14:23:33 2012 +0200
     6.3 @@ -8,13 +8,12 @@
     6.4  
     6.5  
     6.6  import isabelle._
     6.7 -import isabelle.jedit.HTML_Panel
     6.8  
     6.9 -import scala.swing.{Dialog, BorderPanel, Component}
    6.10 -import java.awt.{Point, Dimension}
    6.11 +import scala.swing.{Dialog, BorderPanel, Component, TextArea}
    6.12 +import java.awt.{Font, Point, Dimension}
    6.13  
    6.14  
    6.15 -class Floating_Dialog(private val html: String, _title: String, _location: Point)
    6.16 +class Floating_Dialog(content: XML.Body, _title: String, _location: Point)
    6.17  extends Dialog
    6.18  {    
    6.19    location = _location
    6.20 @@ -24,20 +23,11 @@
    6.21    preferredSize = new Dimension(300, 300)
    6.22    peer.setAlwaysOnTop(true)
    6.23  
    6.24 -  private def render_document(text: String) =
    6.25 -    html_panel.peer.render_document("http://localhost", text)
    6.26 +  private val text_font = new Font(Parameters.font_family, Font.PLAIN, Parameters.font_size)
    6.27 +  private val text = new TextArea
    6.28 +  text.peer.setFont(text_font)
    6.29 +  text.editable = false
    6.30  
    6.31 -  private val html_panel = new Component()
    6.32 -  {
    6.33 -    override lazy val peer: HTML_Panel =
    6.34 -      new HTML_Panel(Parameters.font_family, Parameters.font_size) with SuperMixin
    6.35 -      {
    6.36 -        setPreferredWidth(290)
    6.37 -      }
    6.38 -  }
    6.39 -  
    6.40 -  render_document(html)
    6.41 -  contents = new BorderPanel {
    6.42 -    add(html_panel, BorderPanel.Position.Center)
    6.43 -  }
    6.44 +  contents = new BorderPanel { add(text, BorderPanel.Position.Center) }
    6.45 +  text.text = Pretty.string_of(content, 76, Pretty.font_metric(text.peer.getFontMetrics(text_font)))
    6.46  }
     7.1 --- a/src/Tools/Graphview/src/graph_panel.scala	Wed Sep 26 14:13:07 2012 +0200
     7.2 +++ b/src/Tools/Graphview/src/graph_panel.scala	Wed Sep 26 14:23:33 2012 +0200
     7.3 @@ -203,7 +203,7 @@
     7.4        def moved(at: Point) {
     7.5          val c = Transform.pane_to_graph_coordinates(at)
     7.6          node(c) match {
     7.7 -          case Some(l) => panel.tooltip = vis.Tooltip(l, g.getFontMetrics)
     7.8 +          case Some(l) => panel.tooltip = vis.Tooltip.text(l, g.getFontMetrics)
     7.9            case None => panel.tooltip = null
    7.10          }
    7.11        }
    7.12 @@ -260,7 +260,7 @@
    7.13                  val p = at.clone.asInstanceOf[Point]
    7.14                  SwingUtilities.convertPointToScreen(p, panel.peer)
    7.15                  new Floating_Dialog(
    7.16 -                  vis.Tooltip(l, g.getFontMetrics()),
    7.17 +                  vis.Tooltip.content(l),
    7.18                    vis.Caption(l),
    7.19                    at
    7.20                  ).open
     8.1 --- a/src/Tools/Graphview/src/visualizer.scala	Wed Sep 26 14:13:07 2012 +0200
     8.2 +++ b/src/Tools/Graphview/src/visualizer.scala	Wed Sep 26 14:23:33 2012 +0200
     8.3 @@ -142,14 +142,14 @@
     8.4    }
     8.5    
     8.6    object Tooltip {
     8.7 -    import java.awt.FontMetrics
     8.8 +    def content(name: String): XML.Body = model.complete.get_node(name).content
     8.9  
    8.10 -    def apply(l: String, fm: FontMetrics): String =
    8.11 +    def text(name: String, fm: java.awt.FontMetrics): String =
    8.12      {
    8.13 -      val info = model.complete.get_node(l)
    8.14 -      XML.string_of_body(
    8.15 -        Pretty.formatted(info.content, 76, Pretty.font_metric(fm))
    8.16 -          .map(t => XML.Elem(Markup(HTML.PRE, Nil), HTML.spans(t, false))))
    8.17 +      val txt = Pretty.string_of(content(name), 76, Pretty.font_metric(fm))
    8.18 +      "<html><pre style=\"font-family: " + Parameters.font_family + "; font-size: " +
    8.19 +          Parameters.font_size + "px; \">" +  // FIXME proper scaling (!?)
    8.20 +        HTML.encode(txt) + "</pre></html>"
    8.21      }
    8.22    }
    8.23