support focus_session, for much faster startup of Isabelle/jEdit;
authorwenzelm
Thu Nov 02 10:16:22 2017 +0100 (7 months ago)
changeset 66987352b23c97ac8
parent 66986 5188b1c59434
child 66988 7f8c1dd7576a
support focus_session, for much faster startup of Isabelle/jEdit;
more options for "isabelle jedit";
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	Wed Nov 01 22:13:38 2017 +0100
     1.2 +++ b/NEWS	Thu Nov 02 10:16:22 2017 +0100
     1.3 @@ -34,9 +34,13 @@
     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 +* The command-line tool "isabelle jedit" provides more flexible options:
    1.11 +  - options -B or -P modify the meaning of -l to produce an image on the
    1.12 +    spot or use the session parent image
    1.13 +  - option -F focuses on the specified logic session
    1.14 +  - option -R has changed: it only opens the session ROOT entry
    1.15 +  - option -S sets up the development environment to edit the
    1.16 +    specified session: it abbreviates -B -F -R -l
    1.17  
    1.18  
    1.19  *** HOL ***
     2.1 --- a/src/Doc/JEdit/JEdit.thy	Wed Nov 01 22:13:38 2017 +0100
     2.2 +++ b/src/Doc/JEdit/JEdit.thy	Thu Nov 02 10:16:22 2017 +0100
     2.3 @@ -229,11 +229,13 @@
     2.4  
     2.5    Options are:
     2.6      -B           use base session image, with theories from other sessions
     2.7 +    -F           focus on selected logic session: ignore unrelated theories
     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      -P           use parent session image
    2.12      -R           open ROOT entry of logic session
    2.13 +    -S NAME      edit specified logic session, same as -B -F -R -l NAME
    2.14      -b           build only
    2.15      -d DIR       include session directory
    2.16      -f           fresh build
    2.17 @@ -264,6 +266,14 @@
    2.18    if all required theories are already present there. \<^verbatim>\<open>-P\<close> opens the parent
    2.19    session image directly.
    2.20  
    2.21 +  Option \<^verbatim>\<open>-F\<close> focuses on the specified logic session, as resulting from
    2.22 +  options \<^verbatim>\<open>-l\<close>, \<^verbatim>\<open>-B\<close>, \<^verbatim>\<open>-P\<close>. The accessible name space of theories is
    2.23 +  restricted to sessions that are connected to this session.
    2.24 +
    2.25 +  Option \<^verbatim>\<open>-R\<close> opens the ROOT entry of the specified logic session in the
    2.26 +  editor. Option \<^verbatim>\<open>-S\<close> sets up the development environment to edit the
    2.27 +  specified session: it abbreviates \<^verbatim>\<open>-B\<close> \<^verbatim>\<open>-F\<close> \<^verbatim>\<open>-R\<close> \<^verbatim>\<open>-l\<close>.
    2.28 +
    2.29    The \<^verbatim>\<open>-m\<close> option specifies additional print modes for the prover process.
    2.30    Note that the system option @{system_option_ref jedit_print_mode} allows to
    2.31    do the same persistently (e.g.\ via the \<^emph>\<open>Plugin Options\<close> dialog of
    2.32 @@ -277,9 +287,6 @@
    2.33    The \<^verbatim>\<open>-D\<close> option allows to define JVM system properties; this is passed
    2.34    directly to the underlying \<^verbatim>\<open>java\<close> process.
    2.35  
    2.36 -  Option \<^verbatim>\<open>-R\<close> opens the ROOT entry of the specified logic session in the
    2.37 -  editor.
    2.38 -
    2.39    The \<^verbatim>\<open>-b\<close> and \<^verbatim>\<open>-f\<close> options control the self-build mechanism of
    2.40    Isabelle/jEdit. This is only relevant for building from sources, which also
    2.41    requires an auxiliary \<^verbatim>\<open>jedit_build\<close> component from
     3.1 --- a/src/Pure/Thy/sessions.scala	Wed Nov 01 22:13:38 2017 +0100
     3.2 +++ b/src/Pure/Thy/sessions.scala	Thu Nov 02 10:16:22 2017 +0100
     3.3 @@ -338,6 +338,7 @@
     3.4    def base_info(options: Options, session: String,
     3.5      dirs: List[Path] = Nil,
     3.6      all_known: Boolean = false,
     3.7 +    focus_session: Boolean = false,
     3.8      required_session: Boolean = false): Base_Info =
     3.9    {
    3.10      val full_sessions = load(options, dirs = dirs)
    3.11 @@ -387,7 +388,12 @@
    3.12      val full_sessions1 =
    3.13        if (infos1.isEmpty) full_sessions
    3.14        else load(options, dirs = dirs, infos = infos1)
    3.15 -    val selected_sessions1 = full_sessions1.selection(Selection(sessions = List(session1)))._2
    3.16 +
    3.17 +    val select_sessions1 =
    3.18 +      if (focus_session) full_sessions1.imports_descendants(List(session1))
    3.19 +      else List(session1)
    3.20 +    val selected_sessions1 =
    3.21 +      full_sessions1.selection(Selection(sessions = select_sessions1))._2
    3.22  
    3.23      val sessions1 = if (all_known) full_sessions1 else selected_sessions1
    3.24      val deps1 = Sessions.deps(sessions1, global_theories)
     4.1 --- a/src/Tools/jEdit/lib/Tools/jedit	Wed Nov 01 22:13:38 2017 +0100
     4.2 +++ b/src/Tools/jEdit/lib/Tools/jedit	Thu Nov 02 10:16:22 2017 +0100
     4.3 @@ -98,11 +98,13 @@
     4.4    echo
     4.5    echo "  Options are:"
     4.6    echo "    -B           use base session image, with theories from other sessions"
     4.7 +  echo "    -F           focus on selected logic session: ignore unrelated theories"
     4.8    echo "    -D NAME=X    set JVM system property"
     4.9    echo "    -J OPTION    add JVM runtime option"
    4.10    echo "                 (default $JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS)"
    4.11    echo "    -P           use parent session image"
    4.12    echo "    -R           open ROOT entry of logic session"
    4.13 +  echo "    -S NAME      edit specified logic session, same as abbreviates -B -F -R -l NAME"
    4.14    echo "    -b           build only"
    4.15    echo "    -d DIR       include session directory"
    4.16    echo "    -f           fresh build"
    4.17 @@ -140,6 +142,7 @@
    4.18  BUILD_JARS="jars"
    4.19  ML_PROCESS_POLICY=""
    4.20  JEDIT_LOGIC_BASE=""
    4.21 +JEDIT_LOGIC_FOCUS=""
    4.22  JEDIT_SESSION_DIRS=""
    4.23  JEDIT_LOGIC_ROOT=""
    4.24  JEDIT_LOGIC_PARENT=""
    4.25 @@ -150,7 +153,7 @@
    4.26  function getoptions()
    4.27  {
    4.28    OPTIND=1
    4.29 -  while getopts "BD:J:PRbd:fj:l:m:np:s" OPT
    4.30 +  while getopts "BFD:J:PRS:bd:fj:l:m:np:s" OPT
    4.31    do
    4.32      case "$OPT" in
    4.33        B)
    4.34 @@ -160,6 +163,9 @@
    4.35        D)
    4.36          JAVA_ARGS["${#JAVA_ARGS[@]}"]="-D$OPTARG"
    4.37          ;;
    4.38 +      F)
    4.39 +        JEDIT_LOGIC_FOCUS="true"
    4.40 +        ;;
    4.41        J)
    4.42          JAVA_ARGS["${#JAVA_ARGS[@]}"]="$OPTARG"
    4.43          ;;
    4.44 @@ -170,6 +176,13 @@
    4.45        R)
    4.46          JEDIT_LOGIC_ROOT="true"
    4.47          ;;
    4.48 +      S)
    4.49 +        JEDIT_LOGIC="$OPTARG"
    4.50 +        JEDIT_LOGIC_BASE="true"
    4.51 +        JEDIT_LOGIC_PARENT=""
    4.52 +        JEDIT_LOGIC_FOCUS="true"
    4.53 +        JEDIT_LOGIC_ROOT="true"
    4.54 +        ;;
    4.55        b)
    4.56          BUILD_ONLY=true
    4.57          ;;
    4.58 @@ -411,8 +424,8 @@
    4.59  
    4.60  if [ "$BUILD_ONLY" = false ]
    4.61  then
    4.62 -  export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_LOGIC_BASE JEDIT_LOGIC_PARENT \
    4.63 -    JEDIT_LOGIC_ROOT JEDIT_PRINT_MODE JEDIT_BUILD_MODE
    4.64 +  export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_LOGIC_BASE JEDIT_LOGIC_FOCUS \
    4.65 +    JEDIT_LOGIC_PARENT JEDIT_LOGIC_ROOT JEDIT_PRINT_MODE JEDIT_BUILD_MODE
    4.66    export JEDIT_ML_PROCESS_POLICY="$ML_PROCESS_POLICY"
    4.67    classpath "$JEDIT_HOME/dist/jedit.jar"
    4.68    exec isabelle java "${JAVA_ARGS[@]}" isabelle.Main "${ARGS[@]}"
     5.1 --- a/src/Tools/jEdit/src/jedit_sessions.scala	Wed Nov 01 22:13:38 2017 +0100
     5.2 +++ b/src/Tools/jEdit/src/jedit_sessions.scala	Thu Nov 02 10:16:22 2017 +0100
     5.3 @@ -39,6 +39,7 @@
     5.4        Isabelle_System.getenv("JEDIT_LOGIC"),
     5.5        options.string(jedit_logic_option))
     5.6  
     5.7 +  def logic_focus: Boolean = Isabelle_System.getenv("JEDIT_LOGIC_FOCUS") == "true"
     5.8    def logic_base: Boolean = Isabelle_System.getenv("JEDIT_LOGIC_BASE") == "true"
     5.9    def logic_parent: Boolean = Isabelle_System.getenv("JEDIT_LOGIC_PARENT") == "true"
    5.10  
    5.11 @@ -103,15 +104,14 @@
    5.12    /* session build process */
    5.13  
    5.14    def session_base_info(options: Options): Sessions.Base_Info =
    5.15 -  {
    5.16 -    val logic = logic_name(options)
    5.17 -
    5.18      Sessions.base_info(options,
    5.19 -      if (logic_parent) logic_info(options).flatMap(_.parent) getOrElse logic else logic,
    5.20 +      session =
    5.21 +        if (logic_parent) logic_info(options).flatMap(_.parent) getOrElse logic_name(options)
    5.22 +        else logic_name(options),
    5.23        dirs = JEdit_Sessions.session_dirs(),
    5.24 -      all_known = true,
    5.25 +      all_known = !logic_focus,
    5.26 +      focus_session = logic_focus,
    5.27        required_session = logic_base)
    5.28 -  }
    5.29  
    5.30    def session_build(
    5.31      options: Options, progress: Progress = No_Progress, no_build: Boolean = false): Int =