clarified GUI;

--- 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 ());
 

--- 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 */