# HG changeset patch # User wenzelm # Date 1528114876 -7200 # Node ID bcdc47c9d4af391206e361778c6826f46bc62c0c # Parent 6989752bba4bfed676fbae788a159ba62a122723 clarified signature; simplified options; diff -r 6989752bba4b -r bcdc47c9d4af NEWS --- a/NEWS Sun Jun 03 23:30:53 2018 +0200 +++ b/NEWS Mon Jun 04 14:21:16 2018 +0200 @@ -89,16 +89,16 @@ E.g. "Prob" may be completed to "HOL-Probability.Probability". * The command-line tool "isabelle jedit" provides more flexible options -for session selection: - - options -P opens the parent session image of -l - - options -A and -B modify the meaning of -l to produce a base - image on the spot, based on the specified ancestor (or parent) - - 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 +for session management: + - option -R builds an auxiliary logic image with all required theories + from other sessions, relative to an ancestor session given by option + -A (default: parent) + - option -S is like -R, with a focus on the selected session and its + descendants (this reduces startup time for big projects like AFP) Examples: + isabelle jedit -R HOL-Number_Theory + isabelle jedit -R HOL-Number_Theory -A HOL isabelle jedit -d '$AFP' -S Formal_SSA -A HOL isabelle jedit -d '$AFP' -S Formal_SSA -A HOL-Analysis diff -r 6989752bba4b -r bcdc47c9d4af src/Doc/JEdit/JEdit.thy --- a/src/Doc/JEdit/JEdit.thy Sun Jun 03 23:30:53 2018 +0200 +++ b/src/Doc/JEdit/JEdit.thy Mon Jun 04 14:21:16 2018 +0200 @@ -228,15 +228,12 @@ \Usage: isabelle jedit [OPTIONS] [FILES ...] Options are: - -A specify ancestor for base session image (default: parent) - -B use base session image, with theories from other sessions - -F focus on selected logic session: ignore unrelated theories + -A NAME ancestor session for options -R and -S (default: parent) -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, abbreviates -B -F -R -l NAME + -R NAME build image with requirements from other sessions + -S NAME like option -R, with focus on selected session -b build only -d DIR include session directory -f fresh build @@ -261,18 +258,15 @@ The \<^verbatim>\-n\ option bypasses the implicit build process for the selected session image. - Option \<^verbatim>\-P\ and \<^verbatim>\-B\ and are mutually exclusive and modify the meaning of - option \<^verbatim>\-l\ as follows. Option \<^verbatim>\-P\ opens the parent session image. Option - \<^verbatim>\-B\ prepares a logic image on the spot, based on the required theory - imports from other sessions, relative to an ancestor session given by option - \<^verbatim>\-A\ (default: parent session). + Option \<^verbatim>\-R\ builds an auxiliary logic image with all required theories from + \<^emph>\other\ sessions, relative to an ancestor session given by option \<^verbatim>\-A\ + (default: parent session). Option \<^verbatim>\-R\ also opens the session \<^verbatim>\ROOT\ entry + in the editor, to facilitate editing of the main session. - Option \<^verbatim>\-F\ focuses on the effective logic session: the accessible - namespace of theories is restricted to sessions that are connected to it. - - 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\. + Option \<^verbatim>\-S\ is like \<^verbatim>\-R\, with a focus on the selected session and its + descendants: the namespace of accessible theories is restricted accordingly. + This reduces startup time for big projects, notably the ``Archive of Formal + Proofs''. 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 diff -r 6989752bba4b -r bcdc47c9d4af src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Sun Jun 03 23:30:53 2018 +0200 +++ b/src/Pure/Thy/sessions.scala Mon Jun 04 14:21:16 2018 +0200 @@ -394,21 +394,21 @@ progress: Progress = No_Progress, dirs: List[Path] = Nil, include_sessions: List[String] = Nil, - ancestor_session: Option[String] = None, - all_known: Boolean = false, - focus_session: Boolean = false, - required_session: Boolean = false): Base_Info = + session_ancestor: Option[String] = None, + session_requirements: Boolean = false, + session_focus: Boolean = false, + all_known: Boolean = false): Base_Info = { val full_sessions = load_structure(options, dirs = dirs) val global_theories = full_sessions.global_theories val selected_sessions = - full_sessions.selection(Selection(sessions = session :: ancestor_session.toList)) + full_sessions.selection(Selection(sessions = session :: session_ancestor.toList)) val info = selected_sessions(session) - val ancestor = ancestor_session orElse info.parent + val ancestor = session_ancestor orElse info.parent val (session1, infos1) = - if (required_session && ancestor.isDefined) { + if (session_requirements && ancestor.isDefined) { val deps = Sessions.deps(selected_sessions, global_theories, progress = progress) val base = deps(session) @@ -430,7 +430,7 @@ if (required_theories.isEmpty) (ancestor.get, Nil) else { - val other_name = info.name + "_base(" + ancestor.get + ")" + val other_name = info.name + "_requirements(" + ancestor.get + ")" (other_name, List( make_info(info.options, @@ -461,7 +461,7 @@ { val sel_sessions1 = session1 :: include_sessions val select_sessions1 = - if (focus_session) full_sessions1.imports_descendants(sel_sessions1) else sel_sessions1 + if (session_focus) full_sessions1.imports_descendants(sel_sessions1) else sel_sessions1 full_sessions1.selection(Selection(sessions = select_sessions1)) } diff -r 6989752bba4b -r bcdc47c9d4af src/Tools/jEdit/lib/Tools/jedit --- a/src/Tools/jEdit/lib/Tools/jedit Sun Jun 03 23:30:53 2018 +0200 +++ b/src/Tools/jEdit/lib/Tools/jedit Mon Jun 04 14:21:16 2018 +0200 @@ -97,15 +97,12 @@ echo "Usage: isabelle $PRG [OPTIONS] [FILES ...]" echo echo " Options are:" - echo " -A specify ancestor for base session image (default: parent)" - echo " -B use base session image, with theories from other sessions" - echo " -F focus on selected logic session: ignore unrelated theories" + echo " -A NAME ancestor session for options -R and -S (default: parent)" 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, abbreviates -B -F -R -l NAME" + echo " -R NAME build image with requirements from other sessions" + echo " -S NAME like option -R, with focus on selected session" echo " -b build only" echo " -d DIR include session directory" echo " -f fresh build" @@ -143,11 +140,9 @@ BUILD_JARS="jars" ML_PROCESS_POLICY="" JEDIT_LOGIC_ANCESTOR="" -JEDIT_LOGIC_BASE="" +JEDIT_LOGIC_REQUIREMENTS="" JEDIT_LOGIC_FOCUS="" JEDIT_SESSION_DIRS="" -JEDIT_LOGIC_ROOT="" -JEDIT_LOGIC_PARENT="" JEDIT_LOGIC="" JEDIT_PRINT_MODE="" JEDIT_BUILD_MODE="normal" @@ -155,38 +150,26 @@ function getoptions() { OPTIND=1 - while getopts "A:BFD:J:PRS:bd:fj:l:m:np:s" OPT + while getopts "A:BFD:J:R:S:bd:fj:l:m:np:s" OPT do case "$OPT" in A) JEDIT_LOGIC_ANCESTOR="$OPTARG" ;; - B) - JEDIT_LOGIC_BASE="true" - JEDIT_LOGIC_PARENT="" - ;; D) JAVA_ARGS["${#JAVA_ARGS[@]}"]="-D$OPTARG" ;; - F) - JEDIT_LOGIC_FOCUS="true" - ;; J) JAVA_ARGS["${#JAVA_ARGS[@]}"]="$OPTARG" ;; - P) - JEDIT_LOGIC_PARENT="true" - JEDIT_LOGIC_BASE="" - ;; R) - JEDIT_LOGIC_ROOT="true" + JEDIT_LOGIC="$OPTARG" + JEDIT_LOGIC_REQUIREMENTS="true" ;; S) JEDIT_LOGIC="$OPTARG" - JEDIT_LOGIC_BASE="true" - JEDIT_LOGIC_PARENT="" + JEDIT_LOGIC_REQUIREMENTS="true" JEDIT_LOGIC_FOCUS="true" - JEDIT_LOGIC_ROOT="true" ;; b) BUILD_ONLY=true @@ -429,8 +412,8 @@ if [ "$BUILD_ONLY" = false ] then - export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_LOGIC_ANCESTOR JEDIT_LOGIC_BASE JEDIT_LOGIC_FOCUS \ - JEDIT_LOGIC_PARENT JEDIT_LOGIC_ROOT JEDIT_PRINT_MODE JEDIT_BUILD_MODE + export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_LOGIC_ANCESTOR JEDIT_LOGIC_REQUIREMENTS \ + JEDIT_LOGIC_FOCUS 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 6989752bba4b -r bcdc47c9d4af src/Tools/jEdit/src/jedit_sessions.scala --- a/src/Tools/jEdit/src/jedit_sessions.scala Sun Jun 03 23:30:53 2018 +0200 +++ b/src/Tools/jEdit/src/jedit_sessions.scala Mon Jun 04 14:21:16 2018 +0200 @@ -40,9 +40,8 @@ options.string(jedit_logic_option)) def logic_ancestor: Option[String] = proper_string(Isabelle_System.getenv("JEDIT_LOGIC_ANCESTOR")) + def logic_requirements: Boolean = Isabelle_System.getenv("JEDIT_LOGIC_REQUIREMENTS") == "true" 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" def logic_info(options: Options): Option[Sessions.Info] = try { @@ -52,9 +51,7 @@ catch { case ERROR(_) => None } def logic_root(options: Options): Position.T = - if (Isabelle_System.getenv("JEDIT_LOGIC_ROOT") == "true") { - logic_info(options).map(_.pos) getOrElse Position.none - } + if (logic_requirements) logic_info(options).map(_.pos) getOrElse Position.none else Position.none @@ -111,13 +108,11 @@ def session_base_info(options: Options): Sessions.Base_Info = Sessions.base_info(options, dirs = JEdit_Sessions.session_dirs(), - session = - if (logic_parent) logic_info(options).flatMap(_.parent) getOrElse logic_name(options) - else logic_name(options), - ancestor_session = logic_ancestor, - all_known = !logic_focus, - focus_session = logic_focus, - required_session = logic_base) + session = logic_name(options), + session_ancestor = logic_ancestor, + session_requirements = logic_requirements, + session_focus = logic_focus, + all_known = !logic_focus) def session_build( options: Options, progress: Progress = No_Progress, no_build: Boolean = false): Int =