# HG changeset patch # User wenzelm # Date 1509546727 -3600 # Node ID 829c3133c4ca2ebaa36fd111a95d7e68c7bfe9b5 # Parent f65fc869e83589b1c0b12d2f72007c6e2010ffa1 added isabelle jedit options -B, -P, clarified -R; misc tuning and clarification; diff -r f65fc869e835 -r 829c3133c4ca NEWS --- a/NEWS Wed Nov 01 13:06:01 2017 +0100 +++ b/NEWS Wed Nov 01 15:32:07 2017 +0100 @@ -34,6 +34,10 @@ * 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. + *** HOL *** diff -r f65fc869e835 -r 829c3133c4ca src/Doc/JEdit/JEdit.thy --- a/src/Doc/JEdit/JEdit.thy Wed Nov 01 13:06:01 2017 +0100 +++ b/src/Doc/JEdit/JEdit.thy Wed Nov 01 15:32:07 2017 +0100 @@ -228,10 +228,12 @@ \Usage: isabelle jedit [OPTIONS] [FILES ...] Options are: + -B use image with required theory imports from other sessions -D NAME=X set JVM system property -J OPTION add JVM runtime option (default $JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS) - -R open ROOT entry of logic session and use its parent + -P use parent session image + -R open ROOT entry of logic session -b build only -d DIR include session directory -f fresh build @@ -256,10 +258,11 @@ The \<^verbatim>\-n\ option bypasses the implicit build process for the selected session image. - Option \<^verbatim>\-R\ modifies the meaning of option \<^verbatim>\-l\ as follows: the \<^verbatim>\ROOT\ - 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. + Option \<^verbatim>\-B\ and \<^verbatim>\-P\ are mutually exclusive and modify the meaning of + option \<^verbatim>\-l\ as follows: \<^verbatim>\-B\ prepares a logic image on the spot, based on + the required theory imports from other sessions, or the parent session image + if all required theories are already present there. \<^verbatim>\-P\ opens the parent + session image directly. 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 @@ -274,6 +277,9 @@ 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 f65fc869e835 -r 829c3133c4ca src/Tools/jEdit/lib/Tools/jedit --- a/src/Tools/jEdit/lib/Tools/jedit Wed Nov 01 13:06:01 2017 +0100 +++ b/src/Tools/jEdit/lib/Tools/jedit Wed Nov 01 15:32:07 2017 +0100 @@ -97,10 +97,12 @@ echo "Usage: isabelle $PRG [OPTIONS] [FILES ...]" echo echo " Options are:" + echo " -B use image with required theory imports from other sessions" 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 " -R open ROOT entry of logic session and use its parent" + echo " -P use parent session image" + echo " -R open ROOT entry of logic session" echo " -b build only" echo " -d DIR include session directory" echo " -f fresh build" @@ -137,8 +139,10 @@ BUILD_ONLY=false BUILD_JARS="jars" ML_PROCESS_POLICY="" +JEDIT_LOGIC_BASE="" JEDIT_SESSION_DIRS="" JEDIT_LOGIC_ROOT="" +JEDIT_LOGIC_PARENT="" JEDIT_LOGIC="" JEDIT_PRINT_MODE="" JEDIT_BUILD_MODE="normal" @@ -146,15 +150,23 @@ function getoptions() { OPTIND=1 - while getopts "D:J:Rbd:fj:l:m:np:s" OPT + while getopts "BD:J:PRbd:fj:l:m:np:s" OPT do case "$OPT" in + B) + JEDIT_LOGIC_BASE="true" + JEDIT_LOGIC_PARENT="" + ;; D) JAVA_ARGS["${#JAVA_ARGS[@]}"]="-D$OPTARG" ;; J) JAVA_ARGS["${#JAVA_ARGS[@]}"]="$OPTARG" ;; + P) + JEDIT_LOGIC_PARENT="true" + JEDIT_LOGIC_BASE="" + ;; R) JEDIT_LOGIC_ROOT="true" ;; @@ -399,7 +411,8 @@ if [ "$BUILD_ONLY" = false ] then - export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_LOGIC_ROOT JEDIT_PRINT_MODE JEDIT_BUILD_MODE + export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_LOGIC_BASE 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 f65fc869e835 -r 829c3133c4ca src/Tools/jEdit/src/jedit_resources.scala --- a/src/Tools/jEdit/src/jedit_resources.scala Wed Nov 01 13:06:01 2017 +0100 +++ b/src/Tools/jEdit/src/jedit_resources.scala Wed Nov 01 15:32:07 2017 +0100 @@ -27,9 +27,10 @@ new JEdit_Resources(JEdit_Sessions.session_base_info(options)) } -class JEdit_Resources private(session_base_info: Sessions.Base_Info) +class JEdit_Resources private(val session_base_info: Sessions.Base_Info) extends Resources(session_base_info.base.platform_path) { + def session_name: String = session_base_info.session def session_errors: List[String] = session_base_info.errors diff -r f65fc869e835 -r 829c3133c4ca src/Tools/jEdit/src/jedit_sessions.scala --- a/src/Tools/jEdit/src/jedit_sessions.scala Wed Nov 01 13:06:01 2017 +0100 +++ b/src/Tools/jEdit/src/jedit_sessions.scala Wed Nov 01 15:32:07 2017 +0100 @@ -16,47 +16,56 @@ object JEdit_Sessions { - /* session info */ - - private val option_name = "jedit_logic" - - sealed case class Info(name: String, open_root: Position.T) - - def session_dirs(): List[Path] = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS")) + /* session options */ def session_options(options: Options): Options = Isabelle_System.getenv("JEDIT_ML_PROCESS_POLICY") match { case "" => options - case s => options.string("ML_process_policy") = s + case s => options.string.update("ML_process_policy", s) } - def session_info(options: Options): Info = - { - val logic = - Isabelle_System.default_logic( - Isabelle_System.getenv("JEDIT_LOGIC"), - options.string(option_name)) + def session_dirs(): List[Path] = + Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS")) + + def session_build_mode(): String = Isabelle_System.getenv("JEDIT_BUILD_MODE") + + + /* raw logic info */ + + private val jedit_logic_option = "jedit_logic" + + def logic_name(options: Options): String = + Isabelle_System.default_logic( + Isabelle_System.getenv("JEDIT_LOGIC"), + options.string(jedit_logic_option)) - (for { - sessions <- - try { Some(Sessions.load(session_options(options), dirs = session_dirs())) } - catch { case ERROR(_) => None } - info <- sessions.get(logic) - parent <- info.parent - if Isabelle_System.getenv("JEDIT_LOGIC_ROOT") == "true" - } yield Info(parent, info.pos)) getOrElse Info(logic, Position.none) - } + 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 { Sessions.load(session_options(options), dirs = session_dirs()).get(logic_name(options)) } + catch { case ERROR(_) => None } - def session_name(options: Options): String = session_info(options).name + def logic_root(options: Options): Position.T = + if (Isabelle_System.getenv("JEDIT_LOGIC_ROOT") == "true") { + logic_info(options).map(_.pos) getOrElse Position.none + } + else Position.none + + + /* session base info */ def session_base_info(options: Options): Sessions.Base_Info = { + val logic = logic_name(options) + Sessions.session_base_info(options, - session_name(options), dirs = JEdit_Sessions.session_dirs(), all_known = true) + if (logic_parent) logic_info(options).flatMap(_.parent) getOrElse logic else logic, + dirs = JEdit_Sessions.session_dirs(), + all_known = true, + required_session = logic_base) } - def session_build_mode(): String = Isabelle_System.getenv("JEDIT_BUILD_MODE") - def session_build( options: Options, progress: Progress = No_Progress, no_build: Boolean = false): Int = { @@ -64,24 +73,26 @@ Build.build(options = session_options(options), progress = progress, build_heap = true, no_build = no_build, system_mode = mode == "" || mode == "system", - dirs = session_dirs(), sessions = List(session_name(options))).rc + dirs = session_dirs(), infos = PIDE.resources.session_base_info.infos, + sessions = List(PIDE.resources.session_name)).rc } def session_start(options: Options) { - val modes = - (space_explode(',', options.string("jedit_print_mode")) ::: - space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE"))).reverse - Isabelle_Process.start(PIDE.session, session_options(options), - logic = session_name(options), dirs = session_dirs(), modes = modes, + sessions = Some(PIDE.resources.session_base_info.sessions), + logic = PIDE.resources.session_name, store = Sessions.store(session_build_mode() == "system"), + modes = + (space_explode(',', options.string("jedit_print_mode")) ::: + space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE"))).reverse, phase_changed = PIDE.plugin.session_phase_changed) } def session_list(options: Options): List[String] = { - val sessions = Sessions.load(options, dirs = session_dirs()) + val sessions = + Sessions.load(options, dirs = session_dirs(), infos = PIDE.resources.session_base_info.infos) val (main_sessions, other_sessions) = sessions.imports_topological_order.partition(info => info.groups.contains("main")) main_sessions.map(_.name).sorted ::: other_sessions.map(_.name).sorted @@ -100,21 +111,21 @@ GUI_Thread.require {} val entries = - new Logic_Entry("", "default (" + session_name(options.value) + ")") :: + new Logic_Entry("", "default (" + PIDE.resources.session_name + ")") :: session_list(options.value).map(name => new Logic_Entry(name, name)) val component = new ComboBox(entries) with Option_Component { - name = option_name + name = jedit_logic_option val title = "Logic" def load: Unit = { - val logic = options.string(option_name) + val logic = options.string(jedit_logic_option) entries.find(_.name == logic) match { case Some(entry) => selection.item = entry case None => } } - def save: Unit = options.string(option_name) = selection.item.name + def save: Unit = options.string(jedit_logic_option) = selection.item.name } component.load() diff -r f65fc869e835 -r 829c3133c4ca src/Tools/jEdit/src/plugin.scala --- a/src/Tools/jEdit/src/plugin.scala Wed Nov 01 13:06:01 2017 +0100 +++ b/src/Tools/jEdit/src/plugin.scala Wed Nov 01 15:32:07 2017 +0100 @@ -322,7 +322,7 @@ init_view(view) PIDE.editor.hyperlink_position(true, Document.Snapshot.init, - JEdit_Sessions.session_info(options.value).open_root).foreach(_.follow(view)) + JEdit_Sessions.logic_root(options.value)).foreach(_.follow(view)) case msg: BufferUpdate if msg.getWhat == BufferUpdate.LOAD_STARTED || msg.getWhat == BufferUpdate.CLOSING => diff -r f65fc869e835 -r 829c3133c4ca src/Tools/jEdit/src/session_build.scala --- a/src/Tools/jEdit/src/session_build.scala Wed Nov 01 13:06:01 2017 +0100 +++ b/src/Tools/jEdit/src/session_build.scala Wed Nov 01 15:32:07 2017 +0100 @@ -167,7 +167,7 @@ setVisible(true) Standard_Thread.fork("session_build") { - progress.echo("Build started for Isabelle/" + JEdit_Sessions.session_name(options) + " ...") + progress.echo("Build started for Isabelle/" + PIDE.resources.session_name + " ...") val (out, rc) = try { ("", JEdit_Sessions.session_build(options, progress = progress)) }