clarified signature: prefer selective include_sessions;
authorwenzelm
Thu Mar 22 16:20:53 2018 +0100 (14 months ago)
changeset 679229e668ae81f97
parent 67921 1722384ffd4a
child 67923 3e072441c96a
clarified signature: prefer selective include_sessions;
src/Doc/System/Server.thy
src/Pure/Thy/sessions.scala
src/Pure/Tools/server_commands.scala
     1.1 --- a/src/Doc/System/Server.thy	Thu Mar 22 15:11:14 2018 +0100
     1.2 +++ b/src/Doc/System/Server.thy	Thu Mar 22 16:20:53 2018 +0100
     1.3 @@ -632,7 +632,7 @@
     1.4    \quad~~\<open>preferences?: string,\<close> & \<^bold>\<open>default:\<close> server preferences \\
     1.5    \quad~~\<open>options?: [string],\<close> \\
     1.6    \quad~~\<open>dirs?: [string],\<close> \\
     1.7 -  \quad~~\<open>all_known?: bool,\<close> \\
     1.8 +  \quad~~\<open>include_sessions: [string],\<close> \\
     1.9    \quad~~\<open>system_mode?: bool,\<close> \\
    1.10    \quad~~\<open>verbose?: bool}\<close> \\[2ex]
    1.11    \end{tabular}
    1.12 @@ -694,13 +694,12 @@
    1.13    sessions; see also option \<^verbatim>\<open>-d\<close> in @{tool build}.
    1.14  
    1.15    \<^medskip>
    1.16 -  The \<open>all_known\<close> field set to \<^verbatim>\<open>true\<close> includes all sessions from reachable
    1.17 -  ROOT entries into the name space of theories. This is relevant for proper
    1.18 -  session-qualified names, instead of referring to theory file names. The
    1.19 -  option enables the \<^verbatim>\<open>use_theories\<close> command
    1.20 -  (\secref{sec:command-use-theories}) to refer to arbitrary theories from
    1.21 -  other sessions, but considerable time is required to explore all accessible
    1.22 -  session directories and theory dependencies.
    1.23 +  The \<open>include_sessions\<close> field specifies sessions whose theories should be
    1.24 +  included in the overall name space of session-qualified theory names. This
    1.25 +  corresponds to a \<^bold>\<open>sessions\<close> specification in ROOT files
    1.26 +  (\secref{sec:session-root}). It enables the \<^verbatim>\<open>use_theories\<close> command
    1.27 +  (\secref{sec:command-use-theories}) to refer to sources from other sessions
    1.28 +  in a robust manner, instead of relying on directory locations.
    1.29  
    1.30    \<^medskip>
    1.31    The \<open>system_mode\<close> field set to \<^verbatim>\<open>true\<close> stores resulting session images and
    1.32 @@ -989,24 +988,20 @@
    1.33    @{verbatim [display] \<open>use_theories {"session_id": ..., "theories": ["~~/src/HOL/Isar_Examples/Drinker"]}\<close>}
    1.34  
    1.35    \<^medskip>
    1.36 -  Process some example theories that import other theories via
    1.37 -  session-qualified theory names:
    1.38 -
    1.39 -  @{verbatim [display] \<open>session_start {"session": "HOL", "all_known": true}
    1.40 -use_theories {"session_id": ..., "theories": ["~~/src/HOL/Unix/Unix"]}
    1.41 -session_stop {"session_id": ...}\<close>}
    1.42 -
    1.43 -  The option \<open>all_known\<close> has been used here to the full name space of
    1.44 -  session-qualified theory names accessible in this session. This is also the
    1.45 -  default in Isabelle/jEdit, although it requires significant startup time.
    1.46 -
    1.47 -  \<^medskip>
    1.48    Process some example theories in the context of their (single) parent
    1.49    session:
    1.50  
    1.51    @{verbatim [display] \<open>session_start {"session": "HOL-Library"}
    1.52  use_theories {"session_id": ..., "theories": ["~~/src/HOL/Unix/Unix"]}
    1.53  session_stop {"session_id": ...}\<close>}
    1.54 +
    1.55 +  \<^medskip>
    1.56 +  Process some example theories that import other theories via
    1.57 +  session-qualified theory names:
    1.58 +
    1.59 +  @{verbatim [display] \<open>session_start {"session": "HOL", "include_sessions": ["HOL-Unix"]}
    1.60 +use_theories {"session_id": ..., "theories": ["HOL-Unix.Unix"]}
    1.61 +session_stop {"session_id": ...}\<close>}
    1.62  \<close>
    1.63  
    1.64  end
     2.1 --- a/src/Pure/Thy/sessions.scala	Thu Mar 22 15:11:14 2018 +0100
     2.2 +++ b/src/Pure/Thy/sessions.scala	Thu Mar 22 16:20:53 2018 +0100
     2.3 @@ -373,6 +373,7 @@
     2.4      session: String,
     2.5      progress: Progress = No_Progress,
     2.6      dirs: List[Path] = Nil,
     2.7 +    include_sessions: List[String] = Nil,
     2.8      ancestor_session: Option[String] = None,
     2.9      all_known: Boolean = false,
    2.10      focus_session: Boolean = false,
    2.11 @@ -435,15 +436,17 @@
    2.12        if (infos1.isEmpty) full_sessions
    2.13        else load_structure(options, dirs = dirs, infos = infos1)
    2.14  
    2.15 -    val select_sessions1 =
    2.16 -      if (focus_session) full_sessions1.imports_descendants(List(session1))
    2.17 -      else List(session1)
    2.18      val selected_sessions1 =
    2.19 +    {
    2.20 +      val sel_sessions1 = session1 :: include_sessions
    2.21 +      val select_sessions1 =
    2.22 +        if (focus_session) full_sessions1.imports_descendants(sel_sessions1) else sel_sessions1
    2.23        full_sessions1.selection(Selection(sessions = select_sessions1))
    2.24 +    }
    2.25  
    2.26      val sessions1 = if (all_known) full_sessions1 else selected_sessions1
    2.27      val deps1 = Sessions.deps(sessions1, global_theories, progress = progress)
    2.28 -    val base1 = if (all_known) deps1(session1).copy(known = deps1.all_known) else deps1(session1)
    2.29 +    val base1 = deps1(session1).copy(known = deps1.all_known)
    2.30  
    2.31      Base_Info(options, dirs, session1, sessions1, deps1.errors, base1, infos1)
    2.32    }
     3.1 --- a/src/Pure/Tools/server_commands.scala	Thu Mar 22 15:11:14 2018 +0100
     3.2 +++ b/src/Pure/Tools/server_commands.scala	Thu Mar 22 16:20:53 2018 +0100
     3.3 @@ -40,7 +40,7 @@
     3.4        preferences: String = default_preferences,
     3.5        options: List[String] = Nil,
     3.6        dirs: List[String] = Nil,
     3.7 -      all_known: Boolean = false,
     3.8 +      include_sessions: List[String] = Nil,
     3.9        system_mode: Boolean = false,
    3.10        verbose: Boolean = false)
    3.11  
    3.12 @@ -50,13 +50,13 @@
    3.13          preferences <- JSON.string_default(json, "preferences", default_preferences)
    3.14          options <- JSON.list_default(json, "options", JSON.Value.String.unapply _)
    3.15          dirs <- JSON.list_default(json, "dirs", JSON.Value.String.unapply _)
    3.16 -        all_known <- JSON.bool_default(json, "all_known")
    3.17 +        include_sessions <- JSON.list_default(json, "include_sessions", JSON.Value.String.unapply _)
    3.18          system_mode <- JSON.bool_default(json, "system_mode")
    3.19          verbose <- JSON.bool_default(json, "verbose")
    3.20        }
    3.21        yield {
    3.22          Args(session, preferences = preferences, options = options, dirs = dirs,
    3.23 -          all_known = all_known, system_mode = system_mode, verbose = verbose)
    3.24 +          include_sessions = include_sessions, system_mode = system_mode, verbose = verbose)
    3.25        }
    3.26  
    3.27      def command(args: Args, progress: Progress = No_Progress)
    3.28 @@ -67,7 +67,7 @@
    3.29  
    3.30        val base_info =
    3.31          Sessions.base_info(options, args.session, progress = progress, dirs = dirs,
    3.32 -          all_known = args.all_known)
    3.33 +          include_sessions = args.include_sessions)
    3.34        val base = base_info.check_base
    3.35  
    3.36        val results =