# HG changeset patch
# User wenzelm
# Date 1647971547 -3600
# Node ID d92e0197ba01e84624ac899240d85509b8c777d1
# Parent  38398766be6be94b3b29e04acb98959c69da0ad4
clarified options -l vs. -R;

diff -r 38398766be6b -r d92e0197ba01 src/Doc/JEdit/JEdit.thy
--- 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.
diff -r 38398766be6b -r d92e0197ba01 src/Tools/VSCode/src/vscode_main.scala
--- 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,
diff -r 38398766be6b -r d92e0197ba01 src/Tools/jEdit/lib/Tools/jedit
--- 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