clarified signature;
authorwenzelm
Mon Jun 04 14:21:16 2018 +0200 (16 months ago)
changeset 68370bcdc47c9d4af
parent 68369 6989752bba4b
child 68372 8e9da2d09dc6
child 68374 8740e1241555
clarified signature;
simplified options;
NEWS
src/Doc/JEdit/JEdit.thy
src/Pure/Thy/sessions.scala
src/Tools/jEdit/lib/Tools/jedit
src/Tools/jEdit/src/jedit_sessions.scala
     1.1 --- a/NEWS	Sun Jun 03 23:30:53 2018 +0200
     1.2 +++ b/NEWS	Mon Jun 04 14:21:16 2018 +0200
     1.3 @@ -89,16 +89,16 @@
     1.4  E.g. "Prob" may be completed to "HOL-Probability.Probability".
     1.5  
     1.6  * The command-line tool "isabelle jedit" provides more flexible options
     1.7 -for session selection:
     1.8 -  - options -P opens the parent session image of -l
     1.9 -  - options -A and -B modify the meaning of -l to produce a base
    1.10 -    image on the spot, based on the specified ancestor (or parent)
    1.11 -  - option -F focuses on the specified logic session
    1.12 -  - option -R has changed: it only opens the session ROOT entry
    1.13 -  - option -S sets up the development environment to edit the
    1.14 -    specified session: it abbreviates -B -F -R -l
    1.15 +for session management:
    1.16 +  - option -R builds an auxiliary logic image with all required theories
    1.17 +    from other sessions, relative to an ancestor session given by option
    1.18 +    -A (default: parent)
    1.19 +  - option -S is like -R, with a focus on the selected session and its
    1.20 +    descendants (this reduces startup time for big projects like AFP)
    1.21  
    1.22    Examples:
    1.23 +    isabelle jedit -R HOL-Number_Theory
    1.24 +    isabelle jedit -R HOL-Number_Theory -A HOL
    1.25      isabelle jedit -d '$AFP' -S Formal_SSA -A HOL
    1.26      isabelle jedit -d '$AFP' -S Formal_SSA -A HOL-Analysis
    1.27  
     2.1 --- a/src/Doc/JEdit/JEdit.thy	Sun Jun 03 23:30:53 2018 +0200
     2.2 +++ b/src/Doc/JEdit/JEdit.thy	Mon Jun 04 14:21:16 2018 +0200
     2.3 @@ -228,15 +228,12 @@
     2.4  \<open>Usage: isabelle jedit [OPTIONS] [FILES ...]
     2.5  
     2.6    Options are:
     2.7 -    -A           specify ancestor for base session image (default: parent)
     2.8 -    -B           use base session image, with theories from other sessions
     2.9 -    -F           focus on selected logic session: ignore unrelated theories
    2.10 +    -A NAME      ancestor session for options -R and -S (default: parent)
    2.11      -D NAME=X    set JVM system property
    2.12      -J OPTION    add JVM runtime option
    2.13                   (default $JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS)
    2.14 -    -P           use parent session image
    2.15 -    -R           open ROOT entry of logic session
    2.16 -    -S NAME      edit specified logic session, abbreviates -B -F -R -l NAME
    2.17 +    -R NAME      build image with requirements from other sessions
    2.18 +    -S NAME      like option -R, with focus on selected session
    2.19      -b           build only
    2.20      -d DIR       include session directory
    2.21      -f           fresh build
    2.22 @@ -261,18 +258,15 @@
    2.23    The \<^verbatim>\<open>-n\<close> option bypasses the implicit build process for the selected
    2.24    session image.
    2.25  
    2.26 -  Option \<^verbatim>\<open>-P\<close> and \<^verbatim>\<open>-B\<close> and are mutually exclusive and modify the meaning of
    2.27 -  option \<^verbatim>\<open>-l\<close> as follows. Option \<^verbatim>\<open>-P\<close> opens the parent session image. Option
    2.28 -  \<^verbatim>\<open>-B\<close> prepares a logic image on the spot, based on the required theory
    2.29 -  imports from other sessions, relative to an ancestor session given by option
    2.30 -  \<^verbatim>\<open>-A\<close> (default: parent session).
    2.31 +  Option \<^verbatim>\<open>-R\<close> builds an auxiliary logic image with all required theories from
    2.32 +  \<^emph>\<open>other\<close> sessions, relative to an ancestor session given by option \<^verbatim>\<open>-A\<close>
    2.33 +  (default: parent session). Option \<^verbatim>\<open>-R\<close> also opens the session \<^verbatim>\<open>ROOT\<close> entry
    2.34 +  in the editor, to facilitate editing of the main session.
    2.35  
    2.36 -  Option \<^verbatim>\<open>-F\<close> focuses on the effective logic session: the accessible
    2.37 -  namespace of theories is restricted to sessions that are connected to it.
    2.38 -
    2.39 -  Option \<^verbatim>\<open>-R\<close> opens the ROOT entry of the specified logic session in the
    2.40 -  editor. Option \<^verbatim>\<open>-S\<close> sets up the development environment to edit the
    2.41 -  specified session: it abbreviates \<^verbatim>\<open>-B\<close> \<^verbatim>\<open>-F\<close> \<^verbatim>\<open>-R\<close> \<^verbatim>\<open>-l\<close>.
    2.42 +  Option \<^verbatim>\<open>-S\<close> is like \<^verbatim>\<open>-R\<close>, with a focus on the selected session and its
    2.43 +  descendants: the namespace of accessible theories is restricted accordingly.
    2.44 +  This reduces startup time for big projects, notably the ``Archive of Formal
    2.45 +  Proofs''.
    2.46  
    2.47    The \<^verbatim>\<open>-m\<close> option specifies additional print modes for the prover process.
    2.48    Note that the system option @{system_option_ref jedit_print_mode} allows to
     3.1 --- a/src/Pure/Thy/sessions.scala	Sun Jun 03 23:30:53 2018 +0200
     3.2 +++ b/src/Pure/Thy/sessions.scala	Mon Jun 04 14:21:16 2018 +0200
     3.3 @@ -394,21 +394,21 @@
     3.4      progress: Progress = No_Progress,
     3.5      dirs: List[Path] = Nil,
     3.6      include_sessions: List[String] = Nil,
     3.7 -    ancestor_session: Option[String] = None,
     3.8 -    all_known: Boolean = false,
     3.9 -    focus_session: Boolean = false,
    3.10 -    required_session: Boolean = false): Base_Info =
    3.11 +    session_ancestor: Option[String] = None,
    3.12 +    session_requirements: Boolean = false,
    3.13 +    session_focus: Boolean = false,
    3.14 +    all_known: Boolean = false): Base_Info =
    3.15    {
    3.16      val full_sessions = load_structure(options, dirs = dirs)
    3.17      val global_theories = full_sessions.global_theories
    3.18  
    3.19      val selected_sessions =
    3.20 -      full_sessions.selection(Selection(sessions = session :: ancestor_session.toList))
    3.21 +      full_sessions.selection(Selection(sessions = session :: session_ancestor.toList))
    3.22      val info = selected_sessions(session)
    3.23 -    val ancestor = ancestor_session orElse info.parent
    3.24 +    val ancestor = session_ancestor orElse info.parent
    3.25  
    3.26      val (session1, infos1) =
    3.27 -      if (required_session && ancestor.isDefined) {
    3.28 +      if (session_requirements && ancestor.isDefined) {
    3.29          val deps = Sessions.deps(selected_sessions, global_theories, progress = progress)
    3.30          val base = deps(session)
    3.31  
    3.32 @@ -430,7 +430,7 @@
    3.33  
    3.34          if (required_theories.isEmpty) (ancestor.get, Nil)
    3.35          else {
    3.36 -          val other_name = info.name + "_base(" + ancestor.get + ")"
    3.37 +          val other_name = info.name + "_requirements(" + ancestor.get + ")"
    3.38            (other_name,
    3.39              List(
    3.40                make_info(info.options,
    3.41 @@ -461,7 +461,7 @@
    3.42      {
    3.43        val sel_sessions1 = session1 :: include_sessions
    3.44        val select_sessions1 =
    3.45 -        if (focus_session) full_sessions1.imports_descendants(sel_sessions1) else sel_sessions1
    3.46 +        if (session_focus) full_sessions1.imports_descendants(sel_sessions1) else sel_sessions1
    3.47        full_sessions1.selection(Selection(sessions = select_sessions1))
    3.48      }
    3.49  
     4.1 --- a/src/Tools/jEdit/lib/Tools/jedit	Sun Jun 03 23:30:53 2018 +0200
     4.2 +++ b/src/Tools/jEdit/lib/Tools/jedit	Mon Jun 04 14:21:16 2018 +0200
     4.3 @@ -97,15 +97,12 @@
     4.4    echo "Usage: isabelle $PRG [OPTIONS] [FILES ...]"
     4.5    echo
     4.6    echo "  Options are:"
     4.7 -  echo "    -A           specify ancestor for base session image (default: parent)"
     4.8 -  echo "    -B           use base session image, with theories from other sessions"
     4.9 -  echo "    -F           focus on selected logic session: ignore unrelated theories"
    4.10 +  echo "    -A NAME      ancestor session for options -R and -S (default: parent)"
    4.11    echo "    -D NAME=X    set JVM system property"
    4.12    echo "    -J OPTION    add JVM runtime option"
    4.13    echo "                 (default $JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS)"
    4.14 -  echo "    -P           use parent session image"
    4.15 -  echo "    -R           open ROOT entry of logic session"
    4.16 -  echo "    -S NAME      edit specified logic session, abbreviates -B -F -R -l NAME"
    4.17 +  echo "    -R NAME      build image with requirements from other sessions"
    4.18 +  echo "    -S NAME      like option -R, with focus on selected session"
    4.19    echo "    -b           build only"
    4.20    echo "    -d DIR       include session directory"
    4.21    echo "    -f           fresh build"
    4.22 @@ -143,11 +140,9 @@
    4.23  BUILD_JARS="jars"
    4.24  ML_PROCESS_POLICY=""
    4.25  JEDIT_LOGIC_ANCESTOR=""
    4.26 -JEDIT_LOGIC_BASE=""
    4.27 +JEDIT_LOGIC_REQUIREMENTS=""
    4.28  JEDIT_LOGIC_FOCUS=""
    4.29  JEDIT_SESSION_DIRS=""
    4.30 -JEDIT_LOGIC_ROOT=""
    4.31 -JEDIT_LOGIC_PARENT=""
    4.32  JEDIT_LOGIC=""
    4.33  JEDIT_PRINT_MODE=""
    4.34  JEDIT_BUILD_MODE="normal"
    4.35 @@ -155,38 +150,26 @@
    4.36  function getoptions()
    4.37  {
    4.38    OPTIND=1
    4.39 -  while getopts "A:BFD:J:PRS:bd:fj:l:m:np:s" OPT
    4.40 +  while getopts "A:BFD:J:R:S:bd:fj:l:m:np:s" OPT
    4.41    do
    4.42      case "$OPT" in
    4.43        A)
    4.44          JEDIT_LOGIC_ANCESTOR="$OPTARG"
    4.45          ;;
    4.46 -      B)
    4.47 -        JEDIT_LOGIC_BASE="true"
    4.48 -        JEDIT_LOGIC_PARENT=""
    4.49 -        ;;
    4.50        D)
    4.51          JAVA_ARGS["${#JAVA_ARGS[@]}"]="-D$OPTARG"
    4.52          ;;
    4.53 -      F)
    4.54 -        JEDIT_LOGIC_FOCUS="true"
    4.55 -        ;;
    4.56        J)
    4.57          JAVA_ARGS["${#JAVA_ARGS[@]}"]="$OPTARG"
    4.58          ;;
    4.59 -      P)
    4.60 -        JEDIT_LOGIC_PARENT="true"
    4.61 -        JEDIT_LOGIC_BASE=""
    4.62 -        ;;
    4.63        R)
    4.64 -        JEDIT_LOGIC_ROOT="true"
    4.65 +        JEDIT_LOGIC="$OPTARG"
    4.66 +        JEDIT_LOGIC_REQUIREMENTS="true"
    4.67          ;;
    4.68        S)
    4.69          JEDIT_LOGIC="$OPTARG"
    4.70 -        JEDIT_LOGIC_BASE="true"
    4.71 -        JEDIT_LOGIC_PARENT=""
    4.72 +        JEDIT_LOGIC_REQUIREMENTS="true"
    4.73          JEDIT_LOGIC_FOCUS="true"
    4.74 -        JEDIT_LOGIC_ROOT="true"
    4.75          ;;
    4.76        b)
    4.77          BUILD_ONLY=true
    4.78 @@ -429,8 +412,8 @@
    4.79  
    4.80  if [ "$BUILD_ONLY" = false ]
    4.81  then
    4.82 -  export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_LOGIC_ANCESTOR JEDIT_LOGIC_BASE JEDIT_LOGIC_FOCUS \
    4.83 -    JEDIT_LOGIC_PARENT JEDIT_LOGIC_ROOT JEDIT_PRINT_MODE JEDIT_BUILD_MODE
    4.84 +  export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_LOGIC_ANCESTOR JEDIT_LOGIC_REQUIREMENTS \
    4.85 +    JEDIT_LOGIC_FOCUS JEDIT_PRINT_MODE JEDIT_BUILD_MODE
    4.86    export JEDIT_ML_PROCESS_POLICY="$ML_PROCESS_POLICY"
    4.87    classpath "$JEDIT_HOME/dist/jedit.jar"
    4.88    exec isabelle java "${JAVA_ARGS[@]}" isabelle.Main "${ARGS[@]}"
     5.1 --- a/src/Tools/jEdit/src/jedit_sessions.scala	Sun Jun 03 23:30:53 2018 +0200
     5.2 +++ b/src/Tools/jEdit/src/jedit_sessions.scala	Mon Jun 04 14:21:16 2018 +0200
     5.3 @@ -40,9 +40,8 @@
     5.4        options.string(jedit_logic_option))
     5.5  
     5.6    def logic_ancestor: Option[String] = proper_string(Isabelle_System.getenv("JEDIT_LOGIC_ANCESTOR"))
     5.7 +  def logic_requirements: Boolean = Isabelle_System.getenv("JEDIT_LOGIC_REQUIREMENTS") == "true"
     5.8    def logic_focus: Boolean = Isabelle_System.getenv("JEDIT_LOGIC_FOCUS") == "true"
     5.9 -  def logic_base: Boolean = Isabelle_System.getenv("JEDIT_LOGIC_BASE") == "true"
    5.10 -  def logic_parent: Boolean = Isabelle_System.getenv("JEDIT_LOGIC_PARENT") == "true"
    5.11  
    5.12    def logic_info(options: Options): Option[Sessions.Info] =
    5.13      try {
    5.14 @@ -52,9 +51,7 @@
    5.15      catch { case ERROR(_) => None }
    5.16  
    5.17    def logic_root(options: Options): Position.T =
    5.18 -    if (Isabelle_System.getenv("JEDIT_LOGIC_ROOT") == "true") {
    5.19 -      logic_info(options).map(_.pos) getOrElse Position.none
    5.20 -    }
    5.21 +    if (logic_requirements) logic_info(options).map(_.pos) getOrElse Position.none
    5.22      else Position.none
    5.23  
    5.24  
    5.25 @@ -111,13 +108,11 @@
    5.26    def session_base_info(options: Options): Sessions.Base_Info =
    5.27      Sessions.base_info(options,
    5.28        dirs = JEdit_Sessions.session_dirs(),
    5.29 -      session =
    5.30 -        if (logic_parent) logic_info(options).flatMap(_.parent) getOrElse logic_name(options)
    5.31 -        else logic_name(options),
    5.32 -      ancestor_session = logic_ancestor,
    5.33 -      all_known = !logic_focus,
    5.34 -      focus_session = logic_focus,
    5.35 -      required_session = logic_base)
    5.36 +      session = logic_name(options),
    5.37 +      session_ancestor = logic_ancestor,
    5.38 +      session_requirements = logic_requirements,
    5.39 +      session_focus = logic_focus,
    5.40 +      all_known = !logic_focus)
    5.41  
    5.42    def session_build(
    5.43      options: Options, progress: Progress = No_Progress, no_build: Boolean = false): Int =