# HG changeset patch
# User wenzelm
# Date 1609711597 -3600
# Node ID 4b1cfbf96e36de5413764af83764565980114f25
# Parent  3b14f7315dd2f52fe00e18e6bba7ab129c9c2260
action isabelle.toggle-full-screen;

diff -r 3b14f7315dd2 -r 4b1cfbf96e36 src/Tools/jEdit/src/actions.xml
--- a/src/Tools/jEdit/src/actions.xml	Sun Jan 03 23:01:16 2021 +0100
+++ b/src/Tools/jEdit/src/actions.xml	Sun Jan 03 23:06:37 2021 +0100
@@ -67,6 +67,11 @@
 	    isabelle.jedit.Isabelle.newline(textArea);
 	  </CODE>
 	</ACTION>
+	<ACTION NAME="isabelle.toggle-full-screen">
+	  <CODE>
+	    isabelle.jedit.Isabelle.toggle_full_screen(view);
+	  </CODE>
+	</ACTION>
 	<ACTION NAME="isabelle.goto-entity">
 	  <CODE>
 	    isabelle.jedit.Isabelle.goto_entity(view);
diff -r 3b14f7315dd2 -r 4b1cfbf96e36 src/Tools/jEdit/src/isabelle.scala
--- a/src/Tools/jEdit/src/isabelle.scala	Sun Jan 03 23:01:16 2021 +0100
+++ b/src/Tools/jEdit/src/isabelle.scala	Sun Jan 03 23:06:37 2021 +0100
@@ -9,12 +9,13 @@
 
 import isabelle._
 
-import java.awt.{Frame, Point}
+import java.awt.{Point, Frame, Rectangle}
 
 import scala.swing.CheckBox
 import scala.swing.event.ButtonClicked
 
-import org.gjt.sp.jedit.{jEdit, View, Buffer}
+import org.gjt.sp.jedit.{jEdit, View, Buffer, EditBus}
+import org.gjt.sp.jedit.msg.ViewUpdate
 import org.gjt.sp.jedit.buffer.JEditBuffer
 import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, StructureMatcher, Selection}
 import org.gjt.sp.jedit.syntax.TokenMarker
@@ -227,6 +228,32 @@
   def toggle_node_required(view: View) { Document_Model.view_node_required(view, toggle = true) }
 
 
+  /* full screen */
+
+  // see toggleFullScreen() method in jEdit/org/gjt/sp/jedit/View.java
+  def toggle_full_screen(view: View)
+  {
+    if (Untyped.get[Boolean](view, "fullScreenMode")) view.toggleFullScreen()
+    else {
+      Untyped.set[Boolean](view, "fullScreenMode", true)
+      val screen = GUI.screen_size(view)
+      view.dispose()
+
+      view.updateFullScreenProps()
+      Untyped.set[Rectangle](view, "windowedBounds", view.getBounds)
+      view.setUndecorated(true)
+      view.setBounds(screen.full_screen_bounds)
+      view.validate()
+
+      view.setVisible(true)
+      view.toFront()
+      view.closeAllMenus()
+      view.getEditPane.getTextArea.requestFocus()
+      EditBus.send(new ViewUpdate(view, ViewUpdate.FULL_SCREEN_TOGGLED))
+    }
+  }
+
+
   /* font size */
 
   def reset_font_size() {
diff -r 3b14f7315dd2 -r 4b1cfbf96e36 src/Tools/jEdit/src/jEdit.props
--- a/src/Tools/jEdit/src/jEdit.props	Sun Jan 03 23:01:16 2021 +0100
+++ b/src/Tools/jEdit/src/jEdit.props	Sun Jan 03 23:06:37 2021 +0100
@@ -258,6 +258,8 @@
 isabelle.toggle-breakpoint.label=Toggle Breakpoint
 isabelle.toggle-continuous-checking.label=Toggle continuous checking
 isabelle.toggle-continuous-checking.shortcut=C+e ENTER
+isabelle.toggle-full-screen.label=Toggle full-screen mode
+isabelle.toggle-full-screen.shortcut=F11
 isabelle.toggle-node-required.label=Toggle node required
 isabelle.toggle-node-required.shortcut=C+e SPACE
 isabelle.tooltip.label=Show tooltip