# HG changeset patch # User wenzelm # Date 1509614182 -3600 # Node ID 352b23c97ac860f82c7a641eb52f0eb85964d6af # Parent 5188b1c5943434912b017b91b43b14828ae13cdb support focus_session, for much faster startup of Isabelle/jEdit; more options for "isabelle jedit"; diff -r 5188b1c59434 -r 352b23c97ac8 NEWS --- a/NEWS Wed Nov 01 22:13:38 2017 +0100 +++ b/NEWS Thu Nov 02 10:16:22 2017 +0100 @@ -34,9 +34,13 @@ * Completion supports theory header imports. -* The "isabelle jedit" command-line options -B or -P modify the meaning -of -l to produce an image on the spot or use the session parent image. -Option -R now only opens the session ROOT entry. +* The command-line tool "isabelle jedit" provides more flexible options: + - options -B or -P modify the meaning of -l to produce an image on the + spot or use the session parent image + - option -F focuses on the specified logic session + - option -R has changed: it only opens the session ROOT entry + - option -S sets up the development environment to edit the + specified session: it abbreviates -B -F -R -l *** HOL *** diff -r 5188b1c59434 -r 352b23c97ac8 src/Doc/JEdit/JEdit.thy --- a/src/Doc/JEdit/JEdit.thy Wed Nov 01 22:13:38 2017 +0100 +++ b/src/Doc/JEdit/JEdit.thy Thu Nov 02 10:16:22 2017 +0100 @@ -229,11 +229,13 @@ Options are: -B use base session image, with theories from other sessions + -F focus on selected logic session: ignore unrelated theories -D NAME=X set JVM system property -J OPTION add JVM runtime option (default $JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS) -P use parent session image -R open ROOT entry of logic session + -S NAME edit specified logic session, same as -B -F -R -l NAME -b build only -d DIR include session directory -f fresh build @@ -264,6 +266,14 @@ if all required theories are already present there. \<^verbatim>\-P\ opens the parent session image directly. + Option \<^verbatim>\-F\ focuses on the specified logic session, as resulting from + options \<^verbatim>\-l\, \<^verbatim>\-B\, \<^verbatim>\-P\. The accessible name space of theories is + restricted to sessions that are connected to this session. + + Option \<^verbatim>\-R\ opens the ROOT entry of the specified logic session in the + editor. Option \<^verbatim>\-S\ sets up the development environment to edit the + specified session: it abbreviates \<^verbatim>\-B\ \<^verbatim>\-F\ \<^verbatim>\-R\ \<^verbatim>\-l\. + The \<^verbatim>\-m\ 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>\Plugin Options\ dialog of @@ -277,9 +287,6 @@ The \<^verbatim>\-D\ option allows to define JVM system properties; this is passed directly to the underlying \<^verbatim>\java\ process. - Option \<^verbatim>\-R\ opens the ROOT entry of the specified logic session in the - editor. - The \<^verbatim>\-b\ and \<^verbatim>\-f\ options control the self-build mechanism of Isabelle/jEdit. This is only relevant for building from sources, which also requires an auxiliary \<^verbatim>\jedit_build\ component from diff -r 5188b1c59434 -r 352b23c97ac8 src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Wed Nov 01 22:13:38 2017 +0100 +++ b/src/Pure/Thy/sessions.scala Thu Nov 02 10:16:22 2017 +0100 @@ -338,6 +338,7 @@ def base_info(options: Options, session: String, dirs: List[Path] = Nil, all_known: Boolean = false, + focus_session: Boolean = false, required_session: Boolean = false): Base_Info = { val full_sessions = load(options, dirs = dirs) @@ -387,7 +388,12 @@ val full_sessions1 = if (infos1.isEmpty) full_sessions else load(options, dirs = dirs, infos = infos1) - val selected_sessions1 = full_sessions1.selection(Selection(sessions = List(session1)))._2 + + val select_sessions1 = + if (focus_session) full_sessions1.imports_descendants(List(session1)) + else List(session1) + val selected_sessions1 = + full_sessions1.selection(Selection(sessions = select_sessions1))._2 val sessions1 = if (all_known) full_sessions1 else selected_sessions1 val deps1 = Sessions.deps(sessions1, global_theories) diff -r 5188b1c59434 -r 352b23c97ac8 src/Tools/jEdit/lib/Tools/jedit --- a/src/Tools/jEdit/lib/Tools/jedit Wed Nov 01 22:13:38 2017 +0100 +++ b/src/Tools/jEdit/lib/Tools/jedit Thu Nov 02 10:16:22 2017 +0100 @@ -98,11 +98,13 @@ echo echo " Options are:" echo " -B use base session image, with theories from other sessions" + echo " -F focus on selected logic session: ignore unrelated theories" echo " -D NAME=X set JVM system property" echo " -J OPTION add JVM runtime option" echo " (default $JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS)" echo " -P use parent session image" echo " -R open ROOT entry of logic session" + echo " -S NAME edit specified logic session, same as abbreviates -B -F -R -l NAME" echo " -b build only" echo " -d DIR include session directory" echo " -f fresh build" @@ -140,6 +142,7 @@ BUILD_JARS="jars" ML_PROCESS_POLICY="" JEDIT_LOGIC_BASE="" +JEDIT_LOGIC_FOCUS="" JEDIT_SESSION_DIRS="" JEDIT_LOGIC_ROOT="" JEDIT_LOGIC_PARENT="" @@ -150,7 +153,7 @@ function getoptions() { OPTIND=1 - while getopts "BD:J:PRbd:fj:l:m:np:s" OPT + while getopts "BFD:J:PRS:bd:fj:l:m:np:s" OPT do case "$OPT" in B) @@ -160,6 +163,9 @@ D) JAVA_ARGS["${#JAVA_ARGS[@]}"]="-D$OPTARG" ;; + F) + JEDIT_LOGIC_FOCUS="true" + ;; J) JAVA_ARGS["${#JAVA_ARGS[@]}"]="$OPTARG" ;; @@ -170,6 +176,13 @@ R) JEDIT_LOGIC_ROOT="true" ;; + S) + JEDIT_LOGIC="$OPTARG" + JEDIT_LOGIC_BASE="true" + JEDIT_LOGIC_PARENT="" + JEDIT_LOGIC_FOCUS="true" + JEDIT_LOGIC_ROOT="true" + ;; b) BUILD_ONLY=true ;; @@ -411,8 +424,8 @@ if [ "$BUILD_ONLY" = false ] then - export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_LOGIC_BASE JEDIT_LOGIC_PARENT \ - JEDIT_LOGIC_ROOT JEDIT_PRINT_MODE JEDIT_BUILD_MODE + export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_LOGIC_BASE JEDIT_LOGIC_FOCUS \ + JEDIT_LOGIC_PARENT 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 5188b1c59434 -r 352b23c97ac8 src/Tools/jEdit/src/jedit_sessions.scala --- a/src/Tools/jEdit/src/jedit_sessions.scala Wed Nov 01 22:13:38 2017 +0100 +++ b/src/Tools/jEdit/src/jedit_sessions.scala Thu Nov 02 10:16:22 2017 +0100 @@ -39,6 +39,7 @@ Isabelle_System.getenv("JEDIT_LOGIC"), options.string(jedit_logic_option)) + def logic_focus: Boolean = Isabelle_System.getenv("JEDIT_LOGIC_FOCUS") == "true" def logic_base: Boolean = Isabelle_System.getenv("JEDIT_LOGIC_BASE") == "true" def logic_parent: Boolean = Isabelle_System.getenv("JEDIT_LOGIC_PARENT") == "true" @@ -103,15 +104,14 @@ /* session build process */ def session_base_info(options: Options): Sessions.Base_Info = - { - val logic = logic_name(options) - Sessions.base_info(options, - if (logic_parent) logic_info(options).flatMap(_.parent) getOrElse logic else logic, + session = + if (logic_parent) logic_info(options).flatMap(_.parent) getOrElse logic_name(options) + else logic_name(options), dirs = JEdit_Sessions.session_dirs(), - all_known = true, + all_known = !logic_focus, + focus_session = logic_focus, required_session = logic_base) - } def session_build( options: Options, progress: Progress = No_Progress, no_build: Boolean = false): Int =