Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned signature;
authorwenzelm
Tue, 06 May 2014 17:16:36 +0200
changeset 56880 f8c1d2583699
parent 56879 ee2b61f37ad9
child 56881 15e18540df10
tuned signature;
src/Tools/jEdit/src/output_dockable.scala file | annotate | diff | comparison | revisions
src/Tools/jEdit/src/pretty_text_area.scala file | annotate | diff | comparison | revisions 
--- a/src/Tools/jEdit/src/output_dockable.scala	Tue May 06 16:57:17 2014 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala	Tue May 06 17:16:36 2014 +0200
@@ -142,10 +142,7 @@
 
   private val detach = new Button("Detach") {
     tooltip = "Detach window with static copy of current output"
-    reactions += {
-      case ButtonClicked(_) =>
-        Info_Dockable(view, current_snapshot, current_results, Pretty.separate(current_output))
-    }
+    reactions += { case ButtonClicked(_) => pretty_text_area.detach }
   }
 
   private val controls =
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Tue May 06 16:57:17 2014 +0200
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Tue May 06 17:16:36 2014 +0200
@@ -160,6 +160,12 @@
     refresh()
   }
 
+  def detach
+  {
+    Swing_Thread.require {}
+    Info_Dockable(view, current_base_snapshot, current_base_results, current_body)
+  }
+
 
   /* key handling */
isabelle