added isabelle jedit -R;
errors in session_info/session_content are ignored and deferred to later checks of Build.build;
--- 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
--- 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
--- 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])
{
--- 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[@]}"
--- 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(_))))
}
--- 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 ||