# HG changeset patch
# User wenzelm
# Date 1597317209 -7200
# Node ID d8dd3aa6dae93cf874a4e5339879c4f7374a84f1
# Parent  25db9c4209eee33e7f59aed92d8d04fd17fa5a12
clarified GUI;

diff -r 25db9c4209ee -r d8dd3aa6dae9 src/Pure/PIDE/protocol.ML
--- a/src/Pure/PIDE/protocol.ML	Thu Aug 13 12:59:41 2020 +0200
+++ b/src/Pure/PIDE/protocol.ML	Thu Aug 13 13:13:29 2020 +0200
@@ -172,6 +172,10 @@
         handle exn => if Exn.is_interrupt exn then () (*sic!*) else Exn.reraise exn);
 
 val _ =
+  Isabelle_Process.protocol_command "ML_Heap.full_gc"
+    (fn [] => ML_Heap.full_gc ());
+
+val _ =
   Isabelle_Process.protocol_command "ML_Heap.share_common_data"
     (fn [] => ML_Heap.share_common_data ());
 
diff -r 25db9c4209ee -r d8dd3aa6dae9 src/Tools/jEdit/src/monitor_dockable.scala
--- a/src/Tools/jEdit/src/monitor_dockable.scala	Thu Aug 13 12:59:41 2020 +0200
+++ b/src/Tools/jEdit/src/monitor_dockable.scala	Thu Aug 13 13:13:29 2020 +0200
@@ -93,7 +93,24 @@
     }
   }
 
-  private val controls = Wrap_Panel(List(select_data, limit_data, reset_data))
+  private val full_gc = new Button("GC") {
+    tooltip = "Full garbage collection of ML heap"
+    reactions += {
+      case ButtonClicked(_) =>
+        PIDE.session.protocol_command("ML_Heap.full_gc")
+    }
+  }
+
+  private val share_common_data = new Button("Sharing") {
+    tooltip = "Share common data of ML heap"
+    reactions += {
+      case ButtonClicked(_) =>
+        PIDE.session.protocol_command("ML_Heap.share_common_data")
+    }
+  }
+
+  private val controls =
+    Wrap_Panel(List(select_data, limit_data, reset_data, full_gc, share_common_data))
 
 
   /* layout */