support alternative ancestor session;
authorwenzelm
Thu Nov 02 11:25:37 2017 +0100 (17 months ago)
changeset 669887f8c1dd7576a
parent 66987 352b23c97ac8
child 66989 25665e7775b7
support alternative ancestor session;
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	Thu Nov 02 10:16:22 2017 +0100
     1.2 +++ b/NEWS	Thu Nov 02 11:25:37 2017 +0100
     1.3 @@ -34,14 +34,18 @@
     1.4  
     1.5  * Completion supports theory header imports.
     1.6  
     1.7 -* The command-line tool "isabelle jedit" provides more flexible options:
     1.8 -  - options -B or -P modify the meaning of -l to produce an image on the
     1.9 -    spot or use the session parent image
    1.10 +* The command-line tool "isabelle jedit" provides more flexible options
    1.11 +for session selection:
    1.12 +  - options -P opens the parent session image of -l
    1.13 +  - options -A and -B modify the meaning of -l to produce a base
    1.14 +    image on the spot, based on the specified ancestor (or parent)
    1.15    - option -F focuses on the specified logic session
    1.16    - option -R has changed: it only opens the session ROOT entry
    1.17    - option -S sets up the development environment to edit the
    1.18      specified session: it abbreviates -B -F -R -l
    1.19  
    1.20 +  Example: isabelle jedit -A HOL -S Formal_SSA -d '$AFP'
    1.21 +
    1.22  
    1.23  *** HOL ***
    1.24  
     2.1 --- a/src/Doc/JEdit/JEdit.thy	Thu Nov 02 10:16:22 2017 +0100
     2.2 +++ b/src/Doc/JEdit/JEdit.thy	Thu Nov 02 11:25:37 2017 +0100
     2.3 @@ -228,6 +228,7 @@
     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      -D NAME=X    set JVM system property
    2.11 @@ -260,15 +261,14 @@
    2.12    The \<^verbatim>\<open>-n\<close> option bypasses the implicit build process for the selected
    2.13    session image.
    2.14  
    2.15 -  Option \<^verbatim>\<open>-B\<close> and \<^verbatim>\<open>-P\<close> are mutually exclusive and modify the meaning of
    2.16 -  option \<^verbatim>\<open>-l\<close> as follows: \<^verbatim>\<open>-B\<close> prepares a logic image on the spot, based on
    2.17 -  the required theory imports from other sessions, or the parent session image
    2.18 -  if all required theories are already present there. \<^verbatim>\<open>-P\<close> opens the parent
    2.19 -  session image directly.
    2.20 +  Option \<^verbatim>\<open>-P\<close> and \<^verbatim>\<open>-B\<close> and are mutually exclusive and modify the meaning of
    2.21 +  option \<^verbatim>\<open>-l\<close> as follows. Option \<^verbatim>\<open>-P\<close> opens the parent session image. Option
    2.22 +  \<^verbatim>\<open>-B\<close> prepares a logic image on the spot, based on the required theory
    2.23 +  imports from other sessions, relative to an ancestor session given by option
    2.24 +  \<^verbatim>\<open>-A\<close> (default: parent session).
    2.25  
    2.26 -  Option \<^verbatim>\<open>-F\<close> focuses on the specified logic session, as resulting from
    2.27 -  options \<^verbatim>\<open>-l\<close>, \<^verbatim>\<open>-B\<close>, \<^verbatim>\<open>-P\<close>. The accessible name space of theories is
    2.28 -  restricted to sessions that are connected to this session.
    2.29 +  Option \<^verbatim>\<open>-F\<close> focuses on the effective logic session: the accessible
    2.30 +  namespace of theories is restricted to sessions that are connected to it.
    2.31  
    2.32    Option \<^verbatim>\<open>-R\<close> opens the ROOT entry of the specified logic session in the
    2.33    editor. Option \<^verbatim>\<open>-S\<close> sets up the development environment to edit the
     3.1 --- a/src/Pure/Thy/sessions.scala	Thu Nov 02 10:16:22 2017 +0100
     3.2 +++ b/src/Pure/Thy/sessions.scala	Thu Nov 02 11:25:37 2017 +0100
     3.3 @@ -152,6 +152,7 @@
     3.4    {
     3.5      def is_empty: Boolean = session_bases.isEmpty
     3.6      def apply(name: String): Base = session_bases(name)
     3.7 +    def get(name: String): Option[Base] = session_bases.get(name)
     3.8  
     3.9      def imported_sources(name: String): List[SHA1.Digest] =
    3.10        session_bases(name).imported_sources.map(_._2)
    3.11 @@ -337,6 +338,7 @@
    3.12  
    3.13    def base_info(options: Options, session: String,
    3.14      dirs: List[Path] = Nil,
    3.15 +    ancestor_session: Option[String] = None,
    3.16      all_known: Boolean = false,
    3.17      focus_session: Boolean = false,
    3.18      required_session: Boolean = false): Base_Info =
    3.19 @@ -346,24 +348,30 @@
    3.20  
    3.21      val selected_sessions = full_sessions.selection(Selection(sessions = List(session)))._2
    3.22      val info = selected_sessions(session)
    3.23 +    val ancestor = ancestor_session orElse info.parent
    3.24  
    3.25      val (session1, infos1) =
    3.26 -      if (required_session && info.parent.isDefined) {
    3.27 +      if (required_session && ancestor.isDefined) {
    3.28          val deps = Sessions.deps(selected_sessions, global_theories)
    3.29          val base = deps(session)
    3.30  
    3.31 -        val parent_loaded = deps(info.parent.get).loaded_theories.defined(_)
    3.32 +        val ancestor_loaded =
    3.33 +          deps.get(ancestor.get) match {
    3.34 +            case None =>
    3.35 +              error("Bad ancestor " + quote(ancestor.get) + " for session " + quote(session))
    3.36 +            case Some(ancestor_base) => ancestor_base.loaded_theories.defined(_)
    3.37 +          }
    3.38  
    3.39          val required_theories =
    3.40            for {
    3.41              thy <- base.loaded_theories.keys
    3.42 -            if !parent_loaded(thy) && base.theory_qualifier(thy) != session
    3.43 +            if !ancestor_loaded(thy) && base.theory_qualifier(thy) != session
    3.44            }
    3.45            yield thy
    3.46  
    3.47 -        if (required_theories.isEmpty) (info.parent.get, Nil)
    3.48 +        if (required_theories.isEmpty) (ancestor.get, Nil)
    3.49          else {
    3.50 -          val other_name = info.name + "(base)"
    3.51 +          val other_name = info.name + "_base(" + ancestor.get + ")"
    3.52            (other_name,
    3.53              List(
    3.54                make_info(info.options,
    3.55 @@ -375,7 +383,7 @@
    3.56                    name = other_name,
    3.57                    groups = info.groups,
    3.58                    path = ".",
    3.59 -                  parent = info.parent,
    3.60 +                  parent = ancestor,
    3.61                    description = "Required theory imports from other sessions",
    3.62                    options = Nil,
    3.63                    imports = info.imports,
     4.1 --- a/src/Tools/jEdit/lib/Tools/jedit	Thu Nov 02 10:16:22 2017 +0100
     4.2 +++ b/src/Tools/jEdit/lib/Tools/jedit	Thu Nov 02 11:25:37 2017 +0100
     4.3 @@ -97,6 +97,7 @@
     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 "    -D NAME=X    set JVM system property"
    4.11 @@ -141,6 +142,7 @@
    4.12  BUILD_ONLY=false
    4.13  BUILD_JARS="jars"
    4.14  ML_PROCESS_POLICY=""
    4.15 +JEDIT_LOGIC_ANCESTOR=""
    4.16  JEDIT_LOGIC_BASE=""
    4.17  JEDIT_LOGIC_FOCUS=""
    4.18  JEDIT_SESSION_DIRS=""
    4.19 @@ -153,9 +155,12 @@
    4.20  function getoptions()
    4.21  {
    4.22    OPTIND=1
    4.23 -  while getopts "BFD:J:PRS:bd:fj:l:m:np:s" OPT
    4.24 +  while getopts "A:BFD:J:PRS:bd:fj:l:m:np:s" OPT
    4.25    do
    4.26      case "$OPT" in
    4.27 +      A)
    4.28 +        JEDIT_LOGIC_ANCESTOR="$OPTARG"
    4.29 +        ;;
    4.30        B)
    4.31          JEDIT_LOGIC_BASE="true"
    4.32          JEDIT_LOGIC_PARENT=""
    4.33 @@ -424,7 +429,7 @@
    4.34  
    4.35  if [ "$BUILD_ONLY" = false ]
    4.36  then
    4.37 -  export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_LOGIC_BASE JEDIT_LOGIC_FOCUS \
    4.38 +  export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_LOGIC_ANCESTOR JEDIT_LOGIC_BASE JEDIT_LOGIC_FOCUS \
    4.39      JEDIT_LOGIC_PARENT JEDIT_LOGIC_ROOT JEDIT_PRINT_MODE JEDIT_BUILD_MODE
    4.40    export JEDIT_ML_PROCESS_POLICY="$ML_PROCESS_POLICY"
    4.41    classpath "$JEDIT_HOME/dist/jedit.jar"
     5.1 --- a/src/Tools/jEdit/src/jedit_sessions.scala	Thu Nov 02 10:16:22 2017 +0100
     5.2 +++ b/src/Tools/jEdit/src/jedit_sessions.scala	Thu Nov 02 11:25:37 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_ancestor: Option[String] = proper_string(Isabelle_System.getenv("JEDIT_LOGIC_ANCESTOR"))
     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 @@ -109,6 +110,7 @@
    5.12          if (logic_parent) logic_info(options).flatMap(_.parent) getOrElse logic_name(options)
    5.13          else logic_name(options),
    5.14        dirs = JEdit_Sessions.session_dirs(),
    5.15 +      ancestor_session = logic_ancestor,
    5.16        all_known = !logic_focus,
    5.17        focus_session = logic_focus,
    5.18        required_session = logic_base)