# HG changeset patch
# User wenzelm
# Date 1399562041 -7200
# Node ID 75ba0e310663e2ddfab41cfc1495d50af718b7f2
# Parent 823f1c9795802589a4ecebe012e3288235bf7061# Parent f371418b96411868b8520d5e63856bbdebb8da63
merged
diff -r 823f1c979580 -r 75ba0e310663 src/Pure/General/untyped.scala
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/untyped.scala Thu May 08 17:14:01 2014 +0200
@@ -0,0 +1,23 @@
+/* Title: Pure/General/untyped.scala
+ Module: PIDE
+ Author: Makarius
+
+Untyped, unscoped, unchecked access to JVM objects.
+*/
+
+package isabelle
+
+
+object Untyped
+{
+ def get(obj: AnyRef, x: String): AnyRef =
+ {
+ obj.getClass.getDeclaredFields.find(_.getName == x) match {
+ case Some(field) =>
+ field.setAccessible(true)
+ field.get(obj)
+ case None => error("No field " + quote(x) + " for " + obj)
+ }
+ }
+}
+
diff -r 823f1c979580 -r 75ba0e310663 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML Thu May 08 11:52:46 2014 +0200
+++ b/src/Pure/Isar/proof.ML Thu May 08 17:14:01 2014 +0200
@@ -364,8 +364,12 @@
if verbose orelse mode = Forward then Proof_Context.pretty_context ctxt
else if mode = Backward then Proof_Context.pretty_ctxt ctxt
else [];
+
+ val position_markup = Position.markup (Position.thread_data ()) Markup.position;
in
- [Pretty.str ("proof (" ^ mode_name mode ^ "): depth " ^ string_of_int (level state div 2 - 1)),
+ [Pretty.block
+ [Pretty.mark_str (position_markup, "proof"),
+ Pretty.str (" (" ^ mode_name mode ^ "): depth " ^ string_of_int (level state div 2 - 1))],
Pretty.str ""] @
(if null prt_ctxt then [] else prt_ctxt @ [Pretty.str ""]) @
(if verbose orelse mode = Forward then
diff -r 823f1c979580 -r 75ba0e310663 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala Thu May 08 11:52:46 2014 +0200
+++ b/src/Pure/PIDE/resources.scala Thu May 08 17:14:01 2014 +0200
@@ -28,9 +28,10 @@
def node_name(qualifier: String, raw_path: Path): Document.Node.Name =
{
+ val no_qualifier = "" // FIXME
val path = raw_path.expand
val node = path.implode
- val theory = Long_Name.qualify(qualifier, Thy_Header.thy_name(node).getOrElse(""))
+ val theory = Long_Name.qualify(no_qualifier, Thy_Header.thy_name(node).getOrElse(""))
val master_dir = if (theory == "") "" else path.dir.implode
Document.Node.Name(node, master_dir, theory)
}
@@ -65,8 +66,9 @@
def import_name(qualifier: String, master: Document.Node.Name, s: String): Document.Node.Name =
{
+ val no_qualifier = "" // FIXME
val thy1 = Thy_Header.base_name(s)
- val thy2 = if (Long_Name.is_qualified(thy1)) thy1 else Long_Name.qualify(qualifier, thy1)
+ val thy2 = if (Long_Name.is_qualified(thy1)) thy1 else Long_Name.qualify(no_qualifier, thy1)
(known_theories.get(thy1) orElse
known_theories.get(thy2) orElse
known_theories.get(Long_Name.base_name(thy1))) match {
@@ -79,7 +81,7 @@
else {
val node = append(master.master_dir, Resources.thy_path(path))
val master_dir = append(master.master_dir, path.dir)
- Document.Node.Name(node, master_dir, Long_Name.qualify(qualifier, theory))
+ Document.Node.Name(node, master_dir, Long_Name.qualify(no_qualifier, theory))
}
}
}
diff -r 823f1c979580 -r 75ba0e310663 src/Pure/Tools/find_consts.ML
--- a/src/Pure/Tools/find_consts.ML Thu May 08 11:52:46 2014 +0200
+++ b/src/Pure/Tools/find_consts.ML Thu May 08 17:14:01 2014 +0200
@@ -112,17 +112,18 @@
fold (fn c => (case eval_entry c of NONE => I | SOME rank => cons (rank, c))) constants []
|> sort (prod_ord (rev_order o int_ord) (string_ord o pairself fst))
|> map (apsnd fst o snd);
+
+ val position_markup = Position.markup (Position.thread_data ()) Markup.position;
in
Pretty.block
- (Pretty.keyword1 "find_consts" :: Pretty.brk 1 :: Pretty.str "query:" :: Pretty.fbrk ::
- Pretty.fbreaks (map pretty_criterion raw_criteria)) ::
+ (Pretty.fbreaks
+ (Pretty.mark position_markup (Pretty.keyword1 "find_consts") ::
+ map pretty_criterion raw_criteria)) ::
Pretty.str "" ::
- Pretty.str
- (if null matches
- then "nothing found"
- else "found " ^ string_of_int (length matches) ^ " constant(s):") ::
- Pretty.str "" ::
- grouped 10 Par_List.map (Pretty.item o single o pretty_const ctxt) matches
+ (if null matches then [Pretty.str "found nothing"]
+ else
+ Pretty.str ("found " ^ string_of_int (length matches) ^ " constant(s):") ::
+ grouped 10 Par_List.map (Pretty.item o single o pretty_const ctxt) matches)
end |> Pretty.fbreaks |> curry Pretty.blk 0;
fun find_consts ctxt args = Pretty.writeln (pretty_consts ctxt args);
diff -r 823f1c979580 -r 75ba0e310663 src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML Thu May 08 11:52:46 2014 +0200
+++ b/src/Pure/Tools/find_theorems.ML Thu May 08 17:14:01 2014 +0200
@@ -70,7 +70,7 @@
| Solves => Pretty.str (prfx "solves")
| Simp pat => Pretty.block [Pretty.str (prfx "simp:"), Pretty.brk 1,
Pretty.quote (Syntax.pretty_term ctxt (Term.show_dummy_patterns pat))]
- | Pattern pat => Pretty.enclose (prfx " \"") "\""
+ | Pattern pat => Pretty.enclose (prfx "\"") "\""
[Syntax.pretty_term ctxt (Term.show_dummy_patterns pat)])
end;
@@ -482,15 +482,17 @@
(if returned < found
then " (" ^ string_of_int returned ^ " displayed)"
else ""));
+ val position_markup = Position.markup (Position.thread_data ()) Markup.position;
in
Pretty.block
- (Pretty.keyword1 "find_theorems" :: Pretty.brk 1 :: Pretty.str "query:" :: Pretty.fbrk ::
- Pretty.fbreaks (map (pretty_criterion ctxt) criteria)) ::
+ (Pretty.fbreaks
+ (Pretty.mark position_markup (Pretty.keyword1 "find_theorems") ::
+ map (pretty_criterion ctxt) criteria)) ::
Pretty.str "" ::
- (if null theorems then [Pretty.str "nothing found"]
+ (if null theorems then [Pretty.str "found nothing"]
else
- [Pretty.str (tally_msg ^ ":"), Pretty.str ""] @
- grouped 10 Par_List.map (Pretty.item o single o pretty_thm ctxt) (rev theorems))
+ Pretty.str (tally_msg ^ ":") ::
+ grouped 10 Par_List.map (Pretty.item o single o pretty_thm ctxt) (rev theorems))
end |> Pretty.fbreaks |> curry Pretty.blk 0;
end;
diff -r 823f1c979580 -r 75ba0e310663 src/Pure/build-jars
--- a/src/Pure/build-jars Thu May 08 11:52:46 2014 +0200
+++ b/src/Pure/build-jars Thu May 08 17:14:01 2014 +0200
@@ -37,6 +37,7 @@
General/time.scala
General/timing.scala
General/url.scala
+ General/untyped.scala
General/word.scala
General/xz_file.scala
GUI/color_value.scala
diff -r 823f1c979580 -r 75ba0e310663 src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit Thu May 08 11:52:46 2014 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit Thu May 08 17:14:01 2014 +0200
@@ -30,6 +30,7 @@
"src/jedit_resources.scala"
"src/monitor_dockable.scala"
"src/output_dockable.scala"
+ "src/pide_docking_framework.scala"
"src/plugin.scala"
"src/pretty_text_area.scala"
"src/pretty_tooltip.scala"
diff -r 823f1c979580 -r 75ba0e310663 src/Tools/jEdit/src/dockable.scala
--- a/src/Tools/jEdit/src/dockable.scala Thu May 08 11:52:46 2014 +0200
+++ b/src/Tools/jEdit/src/dockable.scala Thu May 08 17:14:01 2014 +0200
@@ -27,6 +27,8 @@
def set_content(c: Component) { add(c, BorderLayout.CENTER) }
def set_content(c: scala.swing.Component) { add(c.peer, BorderLayout.CENTER) }
+ def detach_operation: Option[() => Unit] = None
+
protected def init() { }
protected def exit() { }
diff -r 823f1c979580 -r 75ba0e310663 src/Tools/jEdit/src/jEdit.props
--- a/src/Tools/jEdit/src/jEdit.props Thu May 08 11:52:46 2014 +0200
+++ b/src/Tools/jEdit/src/jEdit.props Thu May 08 17:14:01 2014 +0200
@@ -266,6 +266,7 @@
view.antiAlias=standard
view.blockCaret=true
view.caretBlink=false
+view.docking.framework=PIDE
view.eolMarkers=false
view.extendedState=0
view.font=IsabelleText
diff -r 823f1c979580 -r 75ba0e310663 src/Tools/jEdit/src/output_dockable.scala
--- a/src/Tools/jEdit/src/output_dockable.scala Thu May 08 11:52:46 2014 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala Thu May 08 17:14:01 2014 +0200
@@ -35,6 +35,8 @@
val pretty_text_area = new Pretty_Text_Area(view)
set_content(pretty_text_area)
+ override val detach_operation = Some(() => pretty_text_area.detach)
+
private def handle_resize()
{
@@ -141,8 +143,7 @@
}
private val controls =
- new Wrap_Panel(Wrap_Panel.Alignment.Right)(
- auto_update, update, pretty_text_area.detach_button,
+ new Wrap_Panel(Wrap_Panel.Alignment.Right)(auto_update, update,
pretty_text_area.search_label, pretty_text_area.search_pattern, zoom)
add(controls.peer, BorderLayout.NORTH)
}
diff -r 823f1c979580 -r 75ba0e310663 src/Tools/jEdit/src/pide_docking_framework.scala
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/pide_docking_framework.scala Thu May 08 17:14:01 2014 +0200
@@ -0,0 +1,72 @@
+/* Title: Tools/jEdit/src/pide_docking_framework.scala
+ Author: Makarius
+
+PIDE docking framework: "Original" with some add-ons.
+*/
+
+package org.gjt.sp.jedit.gui // sic!
+
+
+import isabelle._
+import isabelle.jedit._
+
+import java.awt.event.{ActionListener, ActionEvent}
+import javax.swing.{JPopupMenu, JMenuItem}
+
+import org.gjt.sp.jedit.View
+
+
+class PIDE_Docking_Framework extends DockableWindowManagerProvider
+{
+ override def create(
+ view: View,
+ instance: DockableWindowFactory,
+ config: View.ViewConfig): DockableWindowManager =
+ new DockableWindowManagerImpl(view, instance, config)
+ {
+ override def createPopupMenu(
+ container: DockableWindowContainer,
+ dockable_name: String,
+ clone: Boolean): JPopupMenu =
+ {
+ val menu = super.createPopupMenu(container, dockable_name, clone)
+
+ val detach_operation: Option[() => Unit] =
+ container match {
+ case floating: FloatingWindowContainer =>
+ val entry = Untyped.get(floating, "entry")
+ val win = Untyped.get(entry, "win")
+ win match {
+ case dockable: Dockable => dockable.detach_operation
+ case _ => None
+ }
+
+ case panel: PanelWindowContainer =>
+ val entries =
+ Untyped.get(panel, "dockables").asInstanceOf[java.util.List[AnyRef]].toArray
+ val wins =
+ (for {
+ entry <- entries.iterator
+ if Untyped.get(Untyped.get(entry, "factory"), "name") == dockable_name
+ win = Untyped.get(entry, "win")
+ if win != null
+ } yield win).toList
+ wins match {
+ case List(dockable: Dockable) => dockable.detach_operation
+ case _ => None
+ }
+
+ case _ => None
+ }
+ if (detach_operation.isDefined) {
+ val detach_item = new JMenuItem("Detach")
+ detach_item.addActionListener(new ActionListener {
+ def actionPerformed(evt: ActionEvent) { detach_operation.get.apply() }
+ })
+ menu.add(detach_item)
+ }
+
+ menu
+ }
+ }
+}
diff -r 823f1c979580 -r 75ba0e310663 src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala Thu May 08 11:52:46 2014 +0200
+++ b/src/Tools/jEdit/src/pretty_text_area.scala Thu May 08 17:14:01 2014 +0200
@@ -17,8 +17,7 @@
import java.util.concurrent.{Future => JFuture}
-import scala.swing.event.ButtonClicked
-import scala.swing.{Button, Label, Component}
+import scala.swing.{Label, Component}
import scala.util.matching.Regex
import org.gjt.sp.jedit.{jEdit, View, Registers}
@@ -221,11 +220,6 @@
if (ok) search_pattern_foreground else current_rendering.error_color)
}
- val detach_button: Component = new Button("Detach") {
- tooltip = "Detach window with static copy of current output"
- reactions += { case ButtonClicked(_) => text_area.detach }
- }
-
/* key handling */
diff -r 823f1c979580 -r 75ba0e310663 src/Tools/jEdit/src/query_dockable.scala
--- a/src/Tools/jEdit/src/query_dockable.scala Thu May 08 11:52:46 2014 +0200
+++ b/src/Tools/jEdit/src/query_dockable.scala Thu May 08 17:14:01 2014 +0200
@@ -91,7 +91,7 @@
query_operation.apply_query(List(limit.text, allow_dups.selected.toString, query.getText))
}
- private val query_label = new Label("Query:") {
+ private val query_label = new Label("Find:") {
tooltip =
GUI.tooltip_lines(
"Search criteria for find operation, e.g.\n\"_ = _\" \"op +\" name: Group -name: monoid")
@@ -113,9 +113,10 @@
private val allow_dups = new CheckBox("Duplicates") {
tooltip = "Show all versions of matching theorems"
selected = false
+ reactions += { case ButtonClicked(_) => apply_query() }
}
- private val apply_button = new Button("Apply") {
+ private val apply_button = new Button("Apply") {
tooltip = "Find theorems meeting specified criteria"
reactions += { case ButtonClicked(_) => apply_query() }
}
@@ -123,7 +124,7 @@
private val control_panel =
new Wrap_Panel(Wrap_Panel.Alignment.Right)(
query_label, Component.wrap(query), limit, allow_dups,
- process_indicator.component, apply_button, pretty_text_area.detach_button,
+ process_indicator.component, apply_button,
pretty_text_area.search_label, pretty_text_area.search_pattern)
def select { control_panel.contents += zoom }
@@ -155,7 +156,7 @@
query_operation.apply_query(List(query.getText))
}
- private val query_label = new Label("Query:") {
+ private val query_label = new Label("Find:") {
tooltip = GUI.tooltip_lines("Name / type patterns for constants")
}
@@ -164,15 +165,14 @@
/* GUI page */
- private val apply_button = new Button("Apply") {
+ private val apply_button = new Button("Apply") {
tooltip = "Find constants by name / type patterns"
reactions += { case ButtonClicked(_) => apply_query() }
}
private val control_panel =
new Wrap_Panel(Wrap_Panel.Alignment.Right)(
- query_label, Component.wrap(query), process_indicator.component,
- apply_button, pretty_text_area.detach_button,
+ query_label, Component.wrap(query), process_indicator.component, apply_button,
pretty_text_area.search_label, pretty_text_area.search_pattern)
def select { control_panel.contents += zoom }
@@ -191,8 +191,11 @@
{
/* query */
+ private val process_indicator = new Process_Indicator
+
val query_operation =
- new Query_Operation(PIDE.editor, view, "print_operation", _ => (),
+ new Query_Operation(PIDE.editor, view, "print_operation",
+ consume_status(process_indicator, _),
(snapshot, results, body) =>
pretty_text_area.update(snapshot, results, Pretty.separate(body)))
@@ -246,7 +249,7 @@
/* GUI page */
- private val apply_button = new Button("Apply") {
+ private val apply_button = new Button("Apply") {
tooltip = "Apply to current context"
reactions += { case ButtonClicked(_) => apply_query() }
}
@@ -258,7 +261,7 @@
set_selector()
control_panel.contents.clear
control_panel.contents ++=
- List(query_label, selector, apply_button, pretty_text_area.detach_button,
+ List(query_label, selector, process_indicator.component, apply_button,
pretty_text_area.search_label, pretty_text_area.search_pattern, zoom)
}
@@ -295,6 +298,8 @@
select_operation()
set_content(operations_pane)
+ override val detach_operation = Some(() => get_operation().foreach(_.pretty_text_area.detach))
+
/* resize */
diff -r 823f1c979580 -r 75ba0e310663 src/Tools/jEdit/src/services.xml
--- a/src/Tools/jEdit/src/services.xml Thu May 08 11:52:46 2014 +0200
+++ b/src/Tools/jEdit/src/services.xml Thu May 08 17:14:01 2014 +0200
@@ -5,6 +5,9 @@
+
+ new org.gjt.sp.jedit.gui.PIDE_Docking_Framework();
+
new isabelle.jedit.Isabelle_Encoding();