clarified options -l vs. -R;
--- a/src/Doc/JEdit/JEdit.thy Tue Mar 22 18:12:58 2022 +0100
+++ b/src/Doc/JEdit/JEdit.thy Tue Mar 22 18:52:27 2022 +0100
@@ -263,7 +263,7 @@
session \<^verbatim>\<open>ROOT\<close> entry in the editor to facilitate editing of the main
session. The \<^verbatim>\<open>-A\<close> option specifies and alternative ancestor session for
option \<^verbatim>\<open>-R\<close>: this allows to restructure the hierarchy of session images on
- the spot.
+ the spot. Options \<^verbatim>\<open>-R\<close> and \<^verbatim>\<open>-l\<close> are mutually exclusive.
The \<^verbatim>\<open>-i\<close> option includes additional sessions into the name-space of
theories: multiple occurrences are possible.
--- a/src/Tools/VSCode/src/vscode_main.scala Tue Mar 22 18:12:58 2022 +0100
+++ b/src/Tools/VSCode/src/vscode_main.scala Tue Mar 22 18:52:27 2022 +0100
@@ -142,7 +142,7 @@
"R:" -> (arg => { logic = arg; logic_requirements = true }),
"d:" -> (arg => session_dirs = session_dirs ::: List(Path.explode(arg))),
"i:" -> (arg => include_sessions = include_sessions ::: List(arg)),
- "l:" -> (arg => logic = arg),
+ "l:" -> (arg => { logic = arg; logic_requirements = false }),
"m:" -> (arg => modes = modes ::: List(arg)),
"n" -> (_ => no_build = true),
"o:" -> add_option,
--- a/src/Tools/jEdit/lib/Tools/jedit Tue Mar 22 18:12:58 2022 +0100
+++ b/src/Tools/jEdit/lib/Tools/jedit Tue Mar 22 18:52:27 2022 +0100
@@ -106,6 +106,7 @@
;;
l)
JEDIT_LOGIC="$OPTARG"
+ JEDIT_LOGIC_REQUIREMENTS="false"
;;
m)
if [ -z "$JEDIT_PRINT_MODE" ]; then