added isabelle jedit options -B, -P, clarified -R;
authorwenzelm
Wed Nov 01 15:32:07 2017 +0100 (18 months ago)
changeset 66973829c3133c4ca
parent 66972 f65fc869e835
child 66974 b14c24b31f45
added isabelle jedit options -B, -P, clarified -R;
misc tuning and clarification;
NEWS
src/Doc/JEdit/JEdit.thy
src/Tools/jEdit/lib/Tools/jedit
src/Tools/jEdit/src/jedit_resources.scala
src/Tools/jEdit/src/jedit_sessions.scala
src/Tools/jEdit/src/plugin.scala
src/Tools/jEdit/src/session_build.scala
     1.1 --- a/NEWS	Wed Nov 01 13:06:01 2017 +0100
     1.2 +++ b/NEWS	Wed Nov 01 15:32:07 2017 +0100
     1.3 @@ -34,6 +34,10 @@
     1.4  
     1.5  * Completion supports theory header imports.
     1.6  
     1.7 +* The "isabelle jedit" command-line options -B or -P modify the meaning
     1.8 +of -l to produce an image on the spot or use the session parent image.
     1.9 +Option -R now only opens the session ROOT entry.
    1.10 +
    1.11  
    1.12  *** HOL ***
    1.13  
     2.1 --- a/src/Doc/JEdit/JEdit.thy	Wed Nov 01 13:06:01 2017 +0100
     2.2 +++ b/src/Doc/JEdit/JEdit.thy	Wed Nov 01 15:32:07 2017 +0100
     2.3 @@ -228,10 +228,12 @@
     2.4  \<open>Usage: isabelle jedit [OPTIONS] [FILES ...]
     2.5  
     2.6    Options are:
     2.7 +    -B           use image with required theory imports from other sessions
     2.8      -D NAME=X    set JVM system property
     2.9      -J OPTION    add JVM runtime option
    2.10                   (default $JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS)
    2.11 -    -R           open ROOT entry of logic session and use its parent
    2.12 +    -P           use parent session image
    2.13 +    -R           open ROOT entry of logic session
    2.14      -b           build only
    2.15      -d DIR       include session directory
    2.16      -f           fresh build
    2.17 @@ -256,10 +258,11 @@
    2.18    The \<^verbatim>\<open>-n\<close> option bypasses the implicit build process for the selected
    2.19    session image.
    2.20  
    2.21 -  Option \<^verbatim>\<open>-R\<close> modifies the meaning of option \<^verbatim>\<open>-l\<close> as follows: the \<^verbatim>\<open>ROOT\<close>
    2.22 -  entry of the specified session is opened in the editor, while its parent
    2.23 -  session is used for formal checking. This facilitates maintenance of a
    2.24 -  broken session, by moving the Prover IDE quickly to relevant source files.
    2.25 +  Option \<^verbatim>\<open>-B\<close> and \<^verbatim>\<open>-P\<close> are mutually exclusive and modify the meaning of
    2.26 +  option \<^verbatim>\<open>-l\<close> as follows: \<^verbatim>\<open>-B\<close> prepares a logic image on the spot, based on
    2.27 +  the required theory imports from other sessions, or the parent session image
    2.28 +  if all required theories are already present there. \<^verbatim>\<open>-P\<close> opens the parent
    2.29 +  session image directly.
    2.30  
    2.31    The \<^verbatim>\<open>-m\<close> option specifies additional print modes for the prover process.
    2.32    Note that the system option @{system_option_ref jedit_print_mode} allows to
    2.33 @@ -274,6 +277,9 @@
    2.34    The \<^verbatim>\<open>-D\<close> option allows to define JVM system properties; this is passed
    2.35    directly to the underlying \<^verbatim>\<open>java\<close> process.
    2.36  
    2.37 +  Option \<^verbatim>\<open>-R\<close> opens the ROOT entry of the specified logic session in the
    2.38 +  editor.
    2.39 +
    2.40    The \<^verbatim>\<open>-b\<close> and \<^verbatim>\<open>-f\<close> options control the self-build mechanism of
    2.41    Isabelle/jEdit. This is only relevant for building from sources, which also
    2.42    requires an auxiliary \<^verbatim>\<open>jedit_build\<close> component from
     3.1 --- a/src/Tools/jEdit/lib/Tools/jedit	Wed Nov 01 13:06:01 2017 +0100
     3.2 +++ b/src/Tools/jEdit/lib/Tools/jedit	Wed Nov 01 15:32:07 2017 +0100
     3.3 @@ -97,10 +97,12 @@
     3.4    echo "Usage: isabelle $PRG [OPTIONS] [FILES ...]"
     3.5    echo
     3.6    echo "  Options are:"
     3.7 +  echo "    -B           use image with required theory imports from other sessions"
     3.8    echo "    -D NAME=X    set JVM system property"
     3.9    echo "    -J OPTION    add JVM runtime option"
    3.10    echo "                 (default $JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS)"
    3.11 -  echo "    -R           open ROOT entry of logic session and use its parent"
    3.12 +  echo "    -P           use parent session image"
    3.13 +  echo "    -R           open ROOT entry of logic session"
    3.14    echo "    -b           build only"
    3.15    echo "    -d DIR       include session directory"
    3.16    echo "    -f           fresh build"
    3.17 @@ -137,8 +139,10 @@
    3.18  BUILD_ONLY=false
    3.19  BUILD_JARS="jars"
    3.20  ML_PROCESS_POLICY=""
    3.21 +JEDIT_LOGIC_BASE=""
    3.22  JEDIT_SESSION_DIRS=""
    3.23  JEDIT_LOGIC_ROOT=""
    3.24 +JEDIT_LOGIC_PARENT=""
    3.25  JEDIT_LOGIC=""
    3.26  JEDIT_PRINT_MODE=""
    3.27  JEDIT_BUILD_MODE="normal"
    3.28 @@ -146,15 +150,23 @@
    3.29  function getoptions()
    3.30  {
    3.31    OPTIND=1
    3.32 -  while getopts "D:J:Rbd:fj:l:m:np:s" OPT
    3.33 +  while getopts "BD:J:PRbd:fj:l:m:np:s" OPT
    3.34    do
    3.35      case "$OPT" in
    3.36 +      B)
    3.37 +        JEDIT_LOGIC_BASE="true"
    3.38 +        JEDIT_LOGIC_PARENT=""
    3.39 +        ;;
    3.40        D)
    3.41          JAVA_ARGS["${#JAVA_ARGS[@]}"]="-D$OPTARG"
    3.42          ;;
    3.43        J)
    3.44          JAVA_ARGS["${#JAVA_ARGS[@]}"]="$OPTARG"
    3.45          ;;
    3.46 +      P)
    3.47 +        JEDIT_LOGIC_PARENT="true"
    3.48 +        JEDIT_LOGIC_BASE=""
    3.49 +        ;;
    3.50        R)
    3.51          JEDIT_LOGIC_ROOT="true"
    3.52          ;;
    3.53 @@ -399,7 +411,8 @@
    3.54  
    3.55  if [ "$BUILD_ONLY" = false ]
    3.56  then
    3.57 -  export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_LOGIC_ROOT JEDIT_PRINT_MODE JEDIT_BUILD_MODE
    3.58 +  export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_LOGIC_BASE JEDIT_LOGIC_PARENT \
    3.59 +    JEDIT_LOGIC_ROOT JEDIT_PRINT_MODE JEDIT_BUILD_MODE
    3.60    export JEDIT_ML_PROCESS_POLICY="$ML_PROCESS_POLICY"
    3.61    classpath "$JEDIT_HOME/dist/jedit.jar"
    3.62    exec isabelle java "${JAVA_ARGS[@]}" isabelle.Main "${ARGS[@]}"
     4.1 --- a/src/Tools/jEdit/src/jedit_resources.scala	Wed Nov 01 13:06:01 2017 +0100
     4.2 +++ b/src/Tools/jEdit/src/jedit_resources.scala	Wed Nov 01 15:32:07 2017 +0100
     4.3 @@ -27,9 +27,10 @@
     4.4      new JEdit_Resources(JEdit_Sessions.session_base_info(options))
     4.5  }
     4.6  
     4.7 -class JEdit_Resources private(session_base_info: Sessions.Base_Info)
     4.8 +class JEdit_Resources private(val session_base_info: Sessions.Base_Info)
     4.9    extends Resources(session_base_info.base.platform_path)
    4.10  {
    4.11 +  def session_name: String = session_base_info.session
    4.12    def session_errors: List[String] = session_base_info.errors
    4.13  
    4.14  
     5.1 --- a/src/Tools/jEdit/src/jedit_sessions.scala	Wed Nov 01 13:06:01 2017 +0100
     5.2 +++ b/src/Tools/jEdit/src/jedit_sessions.scala	Wed Nov 01 15:32:07 2017 +0100
     5.3 @@ -16,47 +16,56 @@
     5.4  
     5.5  object JEdit_Sessions
     5.6  {
     5.7 -  /* session info */
     5.8 -
     5.9 -  private val option_name = "jedit_logic"
    5.10 -
    5.11 -  sealed case class Info(name: String, open_root: Position.T)
    5.12 -
    5.13 -  def session_dirs(): List[Path] = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS"))
    5.14 +  /* session options */
    5.15  
    5.16    def session_options(options: Options): Options =
    5.17      Isabelle_System.getenv("JEDIT_ML_PROCESS_POLICY") match {
    5.18        case "" => options
    5.19 -      case s => options.string("ML_process_policy") = s
    5.20 +      case s => options.string.update("ML_process_policy", s)
    5.21      }
    5.22  
    5.23 -  def session_info(options: Options): Info =
    5.24 -  {
    5.25 -    val logic =
    5.26 -      Isabelle_System.default_logic(
    5.27 -        Isabelle_System.getenv("JEDIT_LOGIC"),
    5.28 -        options.string(option_name))
    5.29 +  def session_dirs(): List[Path] =
    5.30 +    Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS"))
    5.31 +
    5.32 +  def session_build_mode(): String = Isabelle_System.getenv("JEDIT_BUILD_MODE")
    5.33 +
    5.34 +
    5.35 +  /* raw logic info */
    5.36 +
    5.37 +  private val jedit_logic_option = "jedit_logic"
    5.38 +
    5.39 +  def logic_name(options: Options): String =
    5.40 +    Isabelle_System.default_logic(
    5.41 +      Isabelle_System.getenv("JEDIT_LOGIC"),
    5.42 +      options.string(jedit_logic_option))
    5.43  
    5.44 -    (for {
    5.45 -      sessions <-
    5.46 -        try { Some(Sessions.load(session_options(options), dirs = session_dirs())) }
    5.47 -        catch { case ERROR(_) => None }
    5.48 -      info <- sessions.get(logic)
    5.49 -      parent <- info.parent
    5.50 -      if Isabelle_System.getenv("JEDIT_LOGIC_ROOT") == "true"
    5.51 -    } yield Info(parent, info.pos)) getOrElse Info(logic, Position.none)
    5.52 -  }
    5.53 +  def logic_base: Boolean = Isabelle_System.getenv("JEDIT_LOGIC_BASE") == "true"
    5.54 +  def logic_parent: Boolean = Isabelle_System.getenv("JEDIT_LOGIC_PARENT") == "true"
    5.55 +
    5.56 +  def logic_info(options: Options): Option[Sessions.Info] =
    5.57 +    try { Sessions.load(session_options(options), dirs = session_dirs()).get(logic_name(options)) }
    5.58 +    catch { case ERROR(_) => None }
    5.59  
    5.60 -  def session_name(options: Options): String = session_info(options).name
    5.61 +  def logic_root(options: Options): Position.T =
    5.62 +    if (Isabelle_System.getenv("JEDIT_LOGIC_ROOT") == "true") {
    5.63 +      logic_info(options).map(_.pos) getOrElse Position.none
    5.64 +    }
    5.65 +    else Position.none
    5.66 +
    5.67 +
    5.68 +  /* session base info */
    5.69  
    5.70    def session_base_info(options: Options): Sessions.Base_Info =
    5.71    {
    5.72 +    val logic = logic_name(options)
    5.73 +
    5.74      Sessions.session_base_info(options,
    5.75 -      session_name(options), dirs = JEdit_Sessions.session_dirs(), all_known = true)
    5.76 +      if (logic_parent) logic_info(options).flatMap(_.parent) getOrElse logic else logic,
    5.77 +      dirs = JEdit_Sessions.session_dirs(),
    5.78 +      all_known = true,
    5.79 +      required_session = logic_base)
    5.80    }
    5.81  
    5.82 -  def session_build_mode(): String = Isabelle_System.getenv("JEDIT_BUILD_MODE")
    5.83 -
    5.84    def session_build(
    5.85      options: Options, progress: Progress = No_Progress, no_build: Boolean = false): Int =
    5.86    {
    5.87 @@ -64,24 +73,26 @@
    5.88  
    5.89      Build.build(options = session_options(options), progress = progress,
    5.90        build_heap = true, no_build = no_build, system_mode = mode == "" || mode == "system",
    5.91 -      dirs = session_dirs(), sessions = List(session_name(options))).rc
    5.92 +      dirs = session_dirs(), infos = PIDE.resources.session_base_info.infos,
    5.93 +      sessions = List(PIDE.resources.session_name)).rc
    5.94    }
    5.95  
    5.96    def session_start(options: Options)
    5.97    {
    5.98 -    val modes =
    5.99 -      (space_explode(',', options.string("jedit_print_mode")) :::
   5.100 -       space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE"))).reverse
   5.101 -
   5.102      Isabelle_Process.start(PIDE.session, session_options(options),
   5.103 -      logic = session_name(options), dirs = session_dirs(), modes = modes,
   5.104 +      sessions = Some(PIDE.resources.session_base_info.sessions),
   5.105 +      logic = PIDE.resources.session_name,
   5.106        store = Sessions.store(session_build_mode() == "system"),
   5.107 +      modes =
   5.108 +        (space_explode(',', options.string("jedit_print_mode")) :::
   5.109 +         space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE"))).reverse,
   5.110        phase_changed = PIDE.plugin.session_phase_changed)
   5.111    }
   5.112  
   5.113    def session_list(options: Options): List[String] =
   5.114    {
   5.115 -    val sessions = Sessions.load(options, dirs = session_dirs())
   5.116 +    val sessions =
   5.117 +      Sessions.load(options, dirs = session_dirs(), infos = PIDE.resources.session_base_info.infos)
   5.118      val (main_sessions, other_sessions) =
   5.119        sessions.imports_topological_order.partition(info => info.groups.contains("main"))
   5.120      main_sessions.map(_.name).sorted ::: other_sessions.map(_.name).sorted
   5.121 @@ -100,21 +111,21 @@
   5.122      GUI_Thread.require {}
   5.123  
   5.124      val entries =
   5.125 -      new Logic_Entry("", "default (" + session_name(options.value) + ")") ::
   5.126 +      new Logic_Entry("", "default (" + PIDE.resources.session_name + ")") ::
   5.127          session_list(options.value).map(name => new Logic_Entry(name, name))
   5.128  
   5.129      val component = new ComboBox(entries) with Option_Component {
   5.130 -      name = option_name
   5.131 +      name = jedit_logic_option
   5.132        val title = "Logic"
   5.133        def load: Unit =
   5.134        {
   5.135 -        val logic = options.string(option_name)
   5.136 +        val logic = options.string(jedit_logic_option)
   5.137          entries.find(_.name == logic) match {
   5.138            case Some(entry) => selection.item = entry
   5.139            case None =>
   5.140          }
   5.141        }
   5.142 -      def save: Unit = options.string(option_name) = selection.item.name
   5.143 +      def save: Unit = options.string(jedit_logic_option) = selection.item.name
   5.144      }
   5.145  
   5.146      component.load()
     6.1 --- a/src/Tools/jEdit/src/plugin.scala	Wed Nov 01 13:06:01 2017 +0100
     6.2 +++ b/src/Tools/jEdit/src/plugin.scala	Wed Nov 01 15:32:07 2017 +0100
     6.3 @@ -322,7 +322,7 @@
     6.4            init_view(view)
     6.5  
     6.6            PIDE.editor.hyperlink_position(true, Document.Snapshot.init,
     6.7 -            JEdit_Sessions.session_info(options.value).open_root).foreach(_.follow(view))
     6.8 +            JEdit_Sessions.logic_root(options.value)).foreach(_.follow(view))
     6.9  
    6.10          case msg: BufferUpdate
    6.11          if msg.getWhat == BufferUpdate.LOAD_STARTED || msg.getWhat == BufferUpdate.CLOSING =>
     7.1 --- a/src/Tools/jEdit/src/session_build.scala	Wed Nov 01 13:06:01 2017 +0100
     7.2 +++ b/src/Tools/jEdit/src/session_build.scala	Wed Nov 01 15:32:07 2017 +0100
     7.3 @@ -167,7 +167,7 @@
     7.4      setVisible(true)
     7.5  
     7.6      Standard_Thread.fork("session_build") {
     7.7 -      progress.echo("Build started for Isabelle/" + JEdit_Sessions.session_name(options) + " ...")
     7.8 +      progress.echo("Build started for Isabelle/" + PIDE.resources.session_name + " ...")
     7.9  
    7.10        val (out, rc) =
    7.11          try { ("", JEdit_Sessions.session_build(options, progress = progress)) }