# HG changeset patch
# User wenzelm
# Date 1742739140 -3600
# Node ID 0811cfce1f5b9ded998f1a40fbf13068391fef91
# Parent  8d9b5289304cd98de798cd8cade106862c8bbd1a
support for "isabelle jedit -o OPTION";

diff -r 8d9b5289304c -r 0811cfce1f5b NEWS
--- a/NEWS	Sat Mar 22 23:03:11 2025 +0100
+++ b/NEWS	Sun Mar 23 15:12:20 2025 +0100
@@ -17,6 +17,20 @@
 vs. State in particular.
 
 
+*** Isabelle/jEdit Prover IDE ***
+
+* The command-line tool "isabelle jedit" now supports option "-o" as in
+"isabelle build", but it takes persistent preferences into account. When
+options are loaded, command-line options take precedence. When options
+are saved, command-line options are ignored, but original preferences
+take precedence. Example:
+
+  isabelle jedit -o threads=1
+
+This runs Isabelle/jEdit with sequential evaluation in ML, without
+affecting stored preferences of option "threads".
+
+
 *** HOL ***
 
 * Theory "HOL.Fun":
diff -r 8d9b5289304c -r 0811cfce1f5b src/Doc/JEdit/JEdit.thy
--- a/src/Doc/JEdit/JEdit.thy	Sat Mar 22 23:03:11 2025 +0100
+++ b/src/Doc/JEdit/JEdit.thy	Sun Mar 23 15:12:20 2025 +0100
@@ -239,10 +239,11 @@
     -f           fresh build
     -i NAME      include session in name-space of theories
     -j OPTION    add jEdit runtime option
-                 (default $JEDIT_OPTIONS)
-    -l NAME      logic image name
+                 (default -reuseview -nobackground -nosplash -log=9)
+    -l NAME      logic session name
     -m MODE      add print mode for output
     -n           no build of session image on startup
+    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
     -p CMD       command prefix for ML process (e.g. NUMA policy)
     -s           system build mode for session image (system_heaps=true)
     -u           user build mode for session image (system_heaps=false)
@@ -286,6 +287,12 @@
   the official Isabelle release already includes a pre-built version of
   Isabelle/jEdit.
 
+  The \<^verbatim>\<open>-o\<close> option is analogous to @{tool build} \<^cite>\<open>"isabelle-system"\<close>,
+  but it takes persistent preferences into account (\secref{sec:options}).
+  When options are loaded, command-line options take precedence. When options
+  are saved, command-line options are ignored (despite subsequent changes),
+  but original preferences take precedence (including subsequent changes).
+
   \<^bigskip>
   It is also possible to connect to an already running Isabelle/jEdit process
   via @{tool_def jedit_client}:
diff -r 8d9b5289304c -r 0811cfce1f5b src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit	Sat Mar 22 23:03:11 2025 +0100
+++ b/src/Tools/jEdit/lib/Tools/jedit	Sun Mar 23 15:12:20 2025 +0100
@@ -28,6 +28,7 @@
   echo "    -l NAME      logic session name"
   echo "    -m MODE      add print mode for output"
   echo "    -n           no build of session image on startup"
+  echo "    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)"
   echo "    -p CMD       command prefix for ML process (e.g. NUMA policy)"
   echo "    -s           system build mode for session image (system_heaps=true)"
   echo "    -u           user build mode for session image (system_heaps=false)"
@@ -64,12 +65,13 @@
 JEDIT_LOGIC=""
 JEDIT_PRINT_MODE=""
 JEDIT_NO_BUILD=""
+JEDIT_ISABELLE_OPTIONS=""
 JEDIT_BUILD_MODE="default"
 
 function getoptions()
 {
   OPTIND=1
-  while getopts "A:BFD:J:R:bd:fi:j:l:m:np:su" OPT
+  while getopts "A:BFD:J:R:bd:fi:j:l:m:no:p:su" OPT
   do
     case "$OPT" in
       A)
@@ -118,6 +120,13 @@
       n)
         JEDIT_NO_BUILD="true"
         ;;
+      o)
+        if [ -z "$JEDIT_ISABELLE_OPTIONS" ]; then
+          JEDIT_ISABELLE_OPTIONS="$OPTARG"
+        else
+          JEDIT_ISABELLE_OPTIONS="$JEDIT_ISABELLE_OPTIONS"$'\x0b'"$OPTARG"
+        fi
+        ;;
       p)
         PROCESS_POLICY="$OPTARG"
         ;;
@@ -162,7 +171,7 @@
   "$ISABELLE_HOME/lib/scripts/java-gui-setup"
 
   export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_LOGIC_ANCESTOR JEDIT_LOGIC_REQUIREMENTS \
-    JEDIT_INCLUDE_SESSIONS JEDIT_PRINT_MODE JEDIT_NO_BUILD JEDIT_BUILD_MODE
+    JEDIT_INCLUDE_SESSIONS JEDIT_PRINT_MODE JEDIT_NO_BUILD JEDIT_ISABELLE_OPTIONS JEDIT_BUILD_MODE
   export JEDIT_PROCESS_POLICY="$PROCESS_POLICY"
   exec isabelle java -splash:"$(platform_path "$ISABELLE_HOME/lib/logo/isabelle.gif")" \
     "${JAVA_ARGS[@]}" isabelle.jedit.JEdit_Main "${ARGS[@]}"
diff -r 8d9b5289304c -r 0811cfce1f5b src/Tools/jEdit/src/main_plugin.scala
--- a/src/Tools/jEdit/src/main_plugin.scala	Sat Mar 22 23:03:11 2025 +0100
+++ b/src/Tools/jEdit/src/main_plugin.scala	Sun Mar 23 15:12:20 2025 +0100
@@ -60,9 +60,16 @@
 class Main_Plugin extends EBPlugin {
   /* options */
 
+  private lazy val initial_options: Options = Options.init()
+
+  private lazy val more_options: List[Options.Spec] =
+    Library.space_explode('\u000b', Isabelle_System.getenv("JEDIT_ISABELLE_OPTIONS"))
+      .map(Options.Spec.make)
+
   private var _options: JEdit_Options = null
-  private def init_options(): Unit =
-    _options = new JEdit_Options(Options.init())
+  private def init_options(): Unit = {
+    _options = new JEdit_Options(initial_options ++ more_options)
+  }
   def options: JEdit_Options = _options
 
 
@@ -452,7 +459,11 @@
     JEdit_Lib.jedit_text_areas().foreach(Completion_Popup.Text_Area.exit)
 
     if (startup_failure.isEmpty) {
-      options.value.save_prefs()
+      val save_options =
+        more_options.foldLeft(options.value) {
+          case (opts, opt) => opts + initial_options.spec(opt.name)
+        }
+      save_options.save_prefs()
       completion_history.value.save()
     }