# HG changeset patch
# User wenzelm
# Date 1482094693 -3600
# Node ID 8edca34657588cb1abea907fba19e6bcbf4d245b
# Parent  37ce6ceacbb7359db08c3ae91806e95c75adf9a3
added isabelle jedit -R;
errors in session_info/session_content are ignored and deferred to later checks of Build.build;

diff -r 37ce6ceacbb7 -r 8edca3465758 NEWS
--- a/NEWS	Sun Dec 18 20:01:24 2016 +0100
+++ b/NEWS	Sun Dec 18 21:58:13 2016 +0100
@@ -6,6 +6,13 @@
 New in this Isabelle version
 ----------------------------
 
+*** Prover IDE -- Isabelle/Scala/jEdit ***
+
+* Command-line invocation "isabelle jedit -R -l LOGIC" opens the ROOT
+entry of the specified logic session in the editor, while its parent is
+used for formal checking.
+
+
 *** HOL ***
 
 * Swapped orientation of congruence rules mod_add_left_eq,
@@ -31,7 +38,7 @@
 
 * The theorem in Permutations has been renamed:
   bij_swap_ompose_bij ~> bij_swap_compose_bij
- 
+
 
 New in Isabelle2016-1 (December 2016)
 -------------------------------------
@@ -92,6 +99,7 @@
 * Solve direct: option "solve_direct_strict_warnings" gives explicit
 warnings for lemma statements with trivial proofs.
 
+
 *** Prover IDE -- Isabelle/Scala/jEdit ***
 
 * More aggressive flushing of machine-generated input, according to
diff -r 37ce6ceacbb7 -r 8edca3465758 src/Doc/JEdit/JEdit.thy
--- a/src/Doc/JEdit/JEdit.thy	Sun Dec 18 20:01:24 2016 +0100
+++ b/src/Doc/JEdit/JEdit.thy	Sun Dec 18 21:58:13 2016 +0100
@@ -233,6 +233,7 @@
   Options are:
     -D NAME=X    set JVM system property
     -J OPTION    add JVM runtime option
+    -R           open ROOT entry of logic session and use its parent
     -b           build only
     -d DIR       include session directory
     -f           fresh build
@@ -256,6 +257,11 @@
   The \<^verbatim>\<open>-n\<close> option bypasses the implicit build process for the selected
   session image.
 
+  Option \<^verbatim>\<open>-R\<close> modifies the meaning of option \<^verbatim>\<open>-l\<close> as follows: the \<^verbatim>\<open>ROOT\<close>
+  entry of the specified session is opened in the editor, while its parent
+  session is used for formal checking. This facilitates maintenance of a
+  broken session, by moving the Prover IDE quickly to relevant source files.
+
   The \<^verbatim>\<open>-m\<close> option specifies additional print modes for the prover process.
   Note that the system option @{system_option_ref jedit_print_mode} allows to
   do the same persistently (e.g.\ via the \<^emph>\<open>Plugin Options\<close> dialog of
diff -r 37ce6ceacbb7 -r 8edca3465758 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sun Dec 18 20:01:24 2016 +0100
+++ b/src/Pure/Tools/build.scala	Sun Dec 18 21:58:13 2016 +0100
@@ -96,12 +96,12 @@
   /* source dependencies and static content */
 
   sealed case class Session_Content(
-    loaded_theories: Set[String],
-    known_theories: Map[String, Document.Node.Name],
-    keywords: Thy_Header.Keywords,
-    syntax: Outer_Syntax,
-    sources: List[(Path, SHA1.Digest)],
-    session_graph: Graph_Display.Graph)
+    loaded_theories: Set[String] = Set.empty,
+    known_theories: Map[String, Document.Node.Name] = Map.empty,
+    keywords: Thy_Header.Keywords = Nil,
+    syntax: Outer_Syntax = Outer_Syntax.empty,
+    sources: List[(Path, SHA1.Digest)] = Nil,
+    session_graph: Graph_Display.Graph = Graph_Display.empty_graph)
 
   sealed case class Deps(deps: Map[String, Session_Content])
   {
diff -r 37ce6ceacbb7 -r 8edca3465758 src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit	Sun Dec 18 20:01:24 2016 +0100
+++ b/src/Tools/jEdit/lib/Tools/jedit	Sun Dec 18 21:58:13 2016 +0100
@@ -98,6 +98,7 @@
   echo "  Options are:"
   echo "    -D NAME=X    set JVM system property"
   echo "    -J OPTION    add JVM runtime option (default $JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS)"
+  echo "    -R           open ROOT entry of logic session and use its parent"
   echo "    -b           build only"
   echo "    -d DIR       include session directory"
   echo "    -f           fresh build"
@@ -135,6 +136,7 @@
 BUILD_JARS="jars"
 ML_PROCESS_POLICY=""
 JEDIT_SESSION_DIRS=""
+JEDIT_LOGIC_ROOT=""
 JEDIT_LOGIC=""
 JEDIT_PRINT_MODE=""
 JEDIT_BUILD_MODE="normal"
@@ -142,7 +144,7 @@
 function getoptions()
 {
   OPTIND=1
-  while getopts "D:J:bd:fj:l:m:np:s" OPT
+  while getopts "D:J:Rbd:fj:l:m:np:s" OPT
   do
     case "$OPT" in
       D)
@@ -151,6 +153,9 @@
       J)
         JAVA_ARGS["${#JAVA_ARGS[@]}"]="$OPTARG"
         ;;
+      R)
+        JEDIT_LOGIC_ROOT="true"
+        ;;
       b)
         BUILD_ONLY=true
         ;;
@@ -365,7 +370,7 @@
 
 if [ "$BUILD_ONLY" = false ]
 then
-  export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_PRINT_MODE JEDIT_BUILD_MODE
+  export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_LOGIC_ROOT JEDIT_PRINT_MODE JEDIT_BUILD_MODE
   export JEDIT_ML_PROCESS_POLICY="$ML_PROCESS_POLICY"
   classpath "$JEDIT_HOME/dist/jedit.jar"
   exec isabelle java "${JAVA_ARGS[@]}" isabelle.Main "${ARGS[@]}"
diff -r 37ce6ceacbb7 -r 8edca3465758 src/Tools/jEdit/src/jedit_sessions.scala
--- a/src/Tools/jEdit/src/jedit_sessions.scala	Sun Dec 18 20:01:24 2016 +0100
+++ b/src/Tools/jEdit/src/jedit_sessions.scala	Sun Dec 18 21:58:13 2016 +0100
@@ -19,10 +19,7 @@
 
   private val option_name = "jedit_logic"
 
-  def session_name(): String =
-    Isabelle_System.default_logic(
-      Isabelle_System.getenv("JEDIT_LOGIC"),
-      PIDE.options.string(option_name))
+  sealed case class Info(name: String, open_root: Position.T)
 
   def session_dirs(): List[Path] = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS"))
 
@@ -32,6 +29,25 @@
       case s => PIDE.options.value.string("ML_process_policy") = s
     }
 
+  def session_info(): Info =
+  {
+    val logic =
+      Isabelle_System.default_logic(
+        Isabelle_System.getenv("JEDIT_LOGIC"),
+        PIDE.options.string(option_name))
+
+    (for {
+      tree <-
+        try { Some(Sessions.load(session_options(), dirs = session_dirs())) }
+        catch { case ERROR(_) => None }
+      info <- tree.lift(logic)
+      parent <- info.parent
+      if Isabelle_System.getenv("JEDIT_LOGIC_ROOT") == "true"
+    } yield Info(parent, info.pos)) getOrElse Info(logic, Position.none)
+  }
+
+  def session_name(): String = session_info().name
+
   def session_build_mode(): String = Isabelle_System.getenv("JEDIT_BUILD_MODE")
 
   def session_build(progress: Progress = Ignore_Progress, no_build: Boolean = false): Int =
@@ -66,7 +82,10 @@
   def session_content(inlined_files: Boolean): Build.Session_Content =
   {
     val content =
-      Build.session_content(PIDE.options.value, inlined_files, session_dirs(), session_name())
+      try {
+        Build.session_content(PIDE.options.value, inlined_files, session_dirs(), session_name())
+      }
+      catch { case ERROR(_) => Build.Session_Content() }
     content.copy(known_theories =
       content.known_theories.mapValues(name => name.map(File.platform_path(_))))
   }
diff -r 37ce6ceacbb7 -r 8edca3465758 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Sun Dec 18 20:01:24 2016 +0100
+++ b/src/Tools/jEdit/src/plugin.scala	Sun Dec 18 21:58:13 2016 +0100
@@ -333,9 +333,14 @@
               "It is for testing only, not for production use.")
           }
 
-          Session_Build.session_build(jEdit.getActiveView())
+          val view = jEdit.getActiveView()
+
+          Session_Build.session_build(view)
 
-          Keymap_Merge.check_dialog(jEdit.getActiveView())
+          Keymap_Merge.check_dialog(view)
+
+          PIDE.editor.hyperlink_position(true, Document.Snapshot.init,
+            JEdit_Sessions.session_info().open_root).foreach(_.follow(view))
 
         case msg: BufferUpdate
         if msg.getWhat == BufferUpdate.LOADED ||