--- a/src/Tools/jEdit/src/jEdit.props Thu May 08 00:14:06 2014 +0200
+++ b/src/Tools/jEdit/src/jEdit.props Thu May 08 11:47:38 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
--- a/src/Tools/jEdit/src/output_dockable.scala Thu May 08 00:14:06 2014 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala Thu May 08 11:47:38 2014 +0200
@@ -143,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)
}
--- a/src/Tools/jEdit/src/pretty_text_area.scala Thu May 08 00:14:06 2014 +0200
+++ b/src/Tools/jEdit/src/pretty_text_area.scala Thu May 08 11:47:38 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 */
--- a/src/Tools/jEdit/src/query_dockable.scala Thu May 08 00:14:06 2014 +0200
+++ b/src/Tools/jEdit/src/query_dockable.scala Thu May 08 11:47:38 2014 +0200
@@ -123,7 +123,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 }
@@ -171,8 +171,7 @@
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 }
@@ -258,7 +257,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, apply_button,
pretty_text_area.search_label, pretty_text_area.search_pattern, zoom)
}