clarified signature: do not expose somewhat accidental internal options;
authorwenzelm
Thu Mar 22 14:42:14 2018 +0100 (14 months ago)
changeset 67919dd90faed43b2
parent 67918 7dc204623770
child 67920 c3c74310154e
clarified signature: do not expose somewhat accidental internal options;
src/Doc/System/Server.thy
src/Pure/Tools/server_commands.scala
     1.1 --- a/src/Doc/System/Server.thy	Thu Mar 22 14:27:32 2018 +0100
     1.2 +++ b/src/Doc/System/Server.thy	Thu Mar 22 14:42:14 2018 +0100
     1.3 @@ -627,13 +627,12 @@
     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>ancestor_session?: string,\<close> \\
     1.8    \quad~~\<open>all_known?: bool,\<close> \\
     1.9 -  \quad~~\<open>focus_session?: bool,\<close> \\
    1.10 -  \quad~~\<open>required_session?: bool,\<close> \\
    1.11    \quad~~\<open>system_mode?: bool,\<close> \\
    1.12    \quad~~\<open>verbose?: bool}\<close> \\[2ex]
    1.13 +  \end{tabular}
    1.14  
    1.15 +  \begin{tabular}{ll}
    1.16    \<^bold>\<open>type\<close> \<open>session_build_result =\<close> \\
    1.17    \quad\<open>{session: string,\<close> \\
    1.18    \quad~~\<open>ok: bool,\<close> \\
    1.19 @@ -669,10 +668,9 @@
    1.20  subsubsection \<open>Arguments\<close>
    1.21  
    1.22  text \<open>
    1.23 -  The \<open>session\<close> field is mandatory. It specifies the target session name:
    1.24 -  either directly (default) or indirectly (if \<open>required_session\<close> is \<^verbatim>\<open>true\<close>).
    1.25 -  The build process will produce all required ancestor images for the
    1.26 -  specified target.
    1.27 +  The \<open>session\<close> field specifies the target session name. The build process
    1.28 +  will produce all required ancestor images according to the overall session
    1.29 +  graph.
    1.30  
    1.31    \<^medskip>
    1.32    The environment of Isabelle system options is determined from \<open>preferences\<close>
    1.33 @@ -691,13 +689,6 @@
    1.34    sessions; see also option \<^verbatim>\<open>-d\<close> in @{tool build}.
    1.35  
    1.36    \<^medskip>
    1.37 -  The \<open>ancestor_session\<close> field specifies an alternative image as starting
    1.38 -  point for the target image. The default is to use the parent session
    1.39 -  according to the ROOT entry; see also option \<^verbatim>\<open>-A\<close> in @{tool jedit}. This
    1.40 -  can lead to a more light-weight build process, by skipping intermediate
    1.41 -  session images of the hierarchy that are not used later on.
    1.42 -
    1.43 -  \<^medskip>
    1.44    The \<open>all_known\<close> field set to \<^verbatim>\<open>true\<close> includes all sessions from reachable
    1.45    ROOT entries into the name space of theories. This is relevant for proper
    1.46    session-qualified names, instead of referring to theory file names. The
    1.47 @@ -707,17 +698,6 @@
    1.48    session directories and theory dependencies.
    1.49  
    1.50    \<^medskip>
    1.51 -  The \<open>focus_session\<close> field set to \<^verbatim>\<open>true\<close> focuses on the target session:
    1.52 -  the accessible name space of theories is restricted to sessions that are
    1.53 -  connected to it in the imports graph.
    1.54 -
    1.55 -  \<^medskip>
    1.56 -  The \<open>required_session\<close> field set to \<^verbatim>\<open>true\<close> indicates that the target image
    1.57 -  should not be the \<open>session\<close>, but its parent (or ancestor according to
    1.58 -  \<open>ancestor_session\<close>). Thus it prepares a session context where theories from
    1.59 -  the \<open>session\<close> itself can be loaded.
    1.60 -
    1.61 -  \<^medskip>
    1.62    The \<open>system_mode\<close> field set to \<^verbatim>\<open>true\<close> stores resulting session images and
    1.63    log files in @{path "$ISABELLE_HOME/heaps"} instead of the default location
    1.64    @{setting ISABELLE_OUTPUT} (which is normally in @{setting
    1.65 @@ -771,9 +751,6 @@
    1.66  
    1.67    Build a session image from the Archive of Formal Proofs:
    1.68    @{verbatim [display] \<open>session_build {"session": "Coinductive", "dirs": ["$AFP_BASE/thys"]}\<close>}
    1.69 -
    1.70 -  Build of a session image of \<^verbatim>\<open>HOL-Number_Theory\<close> directly on top of \<^verbatim>\<open>HOL\<close>:
    1.71 -  @{verbatim [display] \<open>session_build {"session": "HOL-Number_Theory", "ancestor_session": "HOL"}\<close>}
    1.72  \<close>
    1.73  
    1.74  
     2.1 --- a/src/Pure/Tools/server_commands.scala	Thu Mar 22 14:27:32 2018 +0100
     2.2 +++ b/src/Pure/Tools/server_commands.scala	Thu Mar 22 14:42:14 2018 +0100
     2.3 @@ -30,10 +30,7 @@
     2.4        preferences: String = default_preferences,
     2.5        options: List[String] = Nil,
     2.6        dirs: List[String] = Nil,
     2.7 -      ancestor_session: String = "",
     2.8        all_known: Boolean = false,
     2.9 -      focus_session: Boolean = false,
    2.10 -      required_session: Boolean = false,
    2.11        system_mode: Boolean = false,
    2.12        verbose: Boolean = false)
    2.13  
    2.14 @@ -43,17 +40,13 @@
    2.15          preferences <- JSON.string_default(json, "preferences", default_preferences)
    2.16          options <- JSON.list_default(json, "options", JSON.Value.String.unapply _)
    2.17          dirs <- JSON.list_default(json, "dirs", JSON.Value.String.unapply _)
    2.18 -        ancestor_session <- JSON.string_default(json, "ancestor_session")
    2.19          all_known <- JSON.bool_default(json, "all_known")
    2.20 -        focus_session <- JSON.bool_default(json, "focus_session")
    2.21 -        required_session <- JSON.bool_default(json, "required_session")
    2.22          system_mode <- JSON.bool_default(json, "system_mode")
    2.23          verbose <- JSON.bool_default(json, "verbose")
    2.24        }
    2.25        yield {
    2.26          Args(session, preferences = preferences, options = options, dirs = dirs,
    2.27 -          ancestor_session = ancestor_session, all_known = all_known, focus_session = focus_session,
    2.28 -          required_session = required_session, system_mode = system_mode, verbose = verbose)
    2.29 +          all_known = all_known, system_mode = system_mode, verbose = verbose)
    2.30        }
    2.31  
    2.32      def command(args: Args, progress: Progress = No_Progress)
    2.33 @@ -63,14 +56,8 @@
    2.34        val dirs = args.dirs.map(Path.explode(_))
    2.35  
    2.36        val base_info =
    2.37 -        Sessions.base_info(options,
    2.38 -          args.session,
    2.39 -          progress = progress,
    2.40 -          dirs = dirs,
    2.41 -          ancestor_session = proper_string(args.ancestor_session),
    2.42 -          all_known = args.all_known,
    2.43 -          focus_session = args.focus_session,
    2.44 -          required_session = args.required_session)
    2.45 +        Sessions.base_info(options, args.session, progress = progress, dirs = dirs,
    2.46 +          all_known = args.all_known)
    2.47        val base = base_info.check_base
    2.48  
    2.49        val results =