# HG changeset patch
# User wenzelm
# Date 1399542458 -7200
# Node ID 0f3c375fd27c459557733af4f9d4b445ddee3025
# Parent  408b526911f70dc14ee78941f90b3eb420b37851
enable "PIDE" docking framework by default, and rely on its "Detach" menu item;

diff -r 408b526911f7 -r 0f3c375fd27c src/Tools/jEdit/src/jEdit.props
--- 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
diff -r 408b526911f7 -r 0f3c375fd27c src/Tools/jEdit/src/output_dockable.scala
--- 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)
 }
diff -r 408b526911f7 -r 0f3c375fd27c src/Tools/jEdit/src/pretty_text_area.scala
--- 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 */
 
diff -r 408b526911f7 -r 0f3c375fd27c src/Tools/jEdit/src/query_dockable.scala
--- 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)
     }