merged
authorwenzelm
Wed Apr 01 22:40:41 2015 +0200 (2015-04-01)
changeset 599039d70a39d1cf3
parent 59873 2d929c178283
parent 59902 6afbe5a99139
child 59904 9d04e2c188b3
merged
NEWS
src/HOL/ROOT
     1.1 --- a/NEWS	Wed Apr 01 19:17:41 2015 +0200
     1.2 +++ b/NEWS	Wed Apr 01 22:40:41 2015 +0200
     1.3 @@ -6,6 +6,9 @@
     1.4  
     1.5  *** General ***
     1.6  
     1.7 +* Command 'experiment' opens an anonymous locale context with private
     1.8 +naming policy.
     1.9 +
    1.10  * Structural composition of proof methods (meth1; meth2) in Isar
    1.11  corresponds to (tac1 THEN_ALL_NEW tac2) in ML.
    1.12  
    1.13 @@ -340,6 +343,14 @@
    1.14  
    1.15  *** ML ***
    1.16  
    1.17 +* Subtle change of name space policy: undeclared entries are now
    1.18 +considered inaccessible, instead of accessible via the fully-qualified
    1.19 +internal name. This mainly affects Name_Space.intern (and derivatives),
    1.20 +which may produce an unexpected Long_Name.hidden prefix. Note that
    1.21 +contempory applications use the strict Name_Space.check (and
    1.22 +derivatives) instead, which is not affected by the change. Potential
    1.23 +INCOMPATIBILITY in rare applications of Name_Space.intern.
    1.24 +
    1.25  * The main operations to certify logical entities are Thm.ctyp_of and
    1.26  Thm.cterm_of with a local context; old-style global theory variants are
    1.27  available as Thm.global_ctyp_of and Thm.global_cterm_of.
    1.28 @@ -407,6 +418,8 @@
    1.29  * The Isabelle tool "update_cartouches" changes theory files to use
    1.30  cartouches instead of old-style {* verbatim *} or `alt_string` tokens.
    1.31  
    1.32 +* The Isabelle tool "build" provides new options -k and -x.
    1.33 +
    1.34  
    1.35  
    1.36  New in Isabelle2014 (August 2014)
     2.1 --- a/lib/Tools/build	Wed Apr 01 19:17:41 2015 +0200
     2.2 +++ b/lib/Tools/build	Wed Apr 01 22:40:41 2015 +0200
     2.3 @@ -34,11 +34,13 @@
     2.4    echo "    -d DIR       include session directory"
     2.5    echo "    -g NAME      select session group NAME"
     2.6    echo "    -j INT       maximum number of parallel jobs (default 1)"
     2.7 +  echo "    -k KEYWORD   check theory sources for conflicts with proposed keywords"
     2.8    echo "    -l           list session source files"
     2.9    echo "    -n           no build -- test dependencies only"
    2.10    echo "    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)"
    2.11    echo "    -s           system build mode: produce output in ISABELLE_HOME"
    2.12    echo "    -v           verbose"
    2.13 +  echo "    -x SESSION   exclude SESSION and all its descendants"
    2.14    echo
    2.15    echo "  Build and manage Isabelle sessions, depending on implicit"
    2.16    show_settings "  "
    2.17 @@ -68,13 +70,15 @@
    2.18  declare -a INCLUDE_DIRS=()
    2.19  declare -a SESSION_GROUPS=()
    2.20  MAX_JOBS=1
    2.21 +declare -a CHECK_KEYWORDS=()
    2.22  LIST_FILES=false
    2.23  NO_BUILD=false
    2.24  eval "declare -a BUILD_OPTIONS=($ISABELLE_BUILD_OPTIONS)"
    2.25  SYSTEM_MODE=false
    2.26  VERBOSE=false
    2.27 +declare -a EXCLUDE_SESSIONS=()
    2.28  
    2.29 -while getopts "D:Rabcd:g:j:lno:sv" OPT
    2.30 +while getopts "D:Rabcd:g:j:k:lno:svx:" OPT
    2.31  do
    2.32    case "$OPT" in
    2.33      D)
    2.34 @@ -102,6 +106,9 @@
    2.35        check_number "$OPTARG"
    2.36        MAX_JOBS="$OPTARG"
    2.37        ;;
    2.38 +    k)
    2.39 +      CHECK_KEYWORDS["${#CHECK_KEYWORDS[@]}"]="$OPTARG"
    2.40 +      ;;
    2.41      l)
    2.42        LIST_FILES="true"
    2.43        ;;
    2.44 @@ -117,6 +124,9 @@
    2.45      v)
    2.46        VERBOSE="true"
    2.47        ;;
    2.48 +    x)
    2.49 +      EXCLUDE_SESSIONS["${#EXCLUDE_SESSIONS[@]}"]="$OPTARG"
    2.50 +      ;;
    2.51      \?)
    2.52        usage
    2.53        ;;
    2.54 @@ -145,7 +155,8 @@
    2.55    "$REQUIREMENTS" "$ALL_SESSIONS" "$BUILD_HEAP" "$CLEAN_BUILD" "$MAX_JOBS" \
    2.56    "$LIST_FILES" "$NO_BUILD" "$SYSTEM_MODE" "$VERBOSE" \
    2.57    "${INCLUDE_DIRS[@]}" $'\n' "${SELECT_DIRS[@]}" $'\n' \
    2.58 -  "${SESSION_GROUPS[@]}" $'\n' "${BUILD_OPTIONS[@]}" $'\n' "$@"
    2.59 +  "${SESSION_GROUPS[@]}" $'\n' "${CHECK_KEYWORDS[@]}" $'\n' \
    2.60 +  "${BUILD_OPTIONS[@]}" $'\n' "${EXCLUDE_SESSIONS[@]}" $'\n' "$@"
    2.61  RC="$?"
    2.62  
    2.63  if [ "$NO_BUILD" = false -a "$VERBOSE" = true ]; then
     3.1 --- a/lib/Tools/scala	Wed Apr 01 19:17:41 2015 +0200
     3.2 +++ b/lib/Tools/scala	Wed Apr 01 22:40:41 2015 +0200
     3.3 @@ -6,6 +6,12 @@
     3.4  
     3.5  isabelle_admin_build jars || exit $?
     3.6  
     3.7 -isabelle_scala scala -Dfile.encoding=UTF-8 \
     3.8 +declare -a JAVA_ARGS; eval "JAVA_ARGS=($ISABELLE_JAVA_SYSTEM_OPTIONS)"
     3.9 +declare -a SCALA_ARGS=()
    3.10 +for ARG in "${JAVA_ARGS[@]}"
    3.11 +do
    3.12 +  SCALA_ARGS["${#SCALA_ARGS[@]}"]="-J$ARG"
    3.13 +done
    3.14 +
    3.15 +isabelle_scala scala "${SCALA_ARGS[@]}" \
    3.16    -classpath "$(jvmpath "$ISABELLE_CLASSPATH")" "$@"
    3.17 -
     4.1 --- a/src/Doc/Implementation/Logic.thy	Wed Apr 01 19:17:41 2015 +0200
     4.2 +++ b/src/Doc/Implementation/Logic.thy	Wed Apr 01 22:40:41 2015 +0200
     4.3 @@ -982,7 +982,7 @@
     4.4  theorem (in empty) false: False
     4.5    using bad by blast
     4.6  
     4.7 -ML \<open>@{assert} (Thm.extra_shyps @{thm false} = [@{sort empty}])\<close>
     4.8 +ML_val \<open>@{assert} (Thm.extra_shyps @{thm false} = [@{sort empty}])\<close>
     4.9  
    4.10  text \<open>Thanks to the inference kernel managing sort hypothesis
    4.11    according to their logical significance, this example is merely an
     5.1 --- a/src/Doc/Implementation/ML.thy	Wed Apr 01 19:17:41 2015 +0200
     5.2 +++ b/src/Doc/Implementation/ML.thy	Wed Apr 01 22:40:41 2015 +0200
     5.3 @@ -736,7 +736,7 @@
     5.4  text %mlex \<open>The following artificial examples show how to produce
     5.5    adhoc output of ML values for debugging purposes.\<close>
     5.6  
     5.7 -ML \<open>
     5.8 +ML_val \<open>
     5.9    val x = 42;
    5.10    val y = true;
    5.11  
    5.12 @@ -928,7 +928,7 @@
    5.13    list.
    5.14  \<close>
    5.15  
    5.16 -ML \<open>
    5.17 +ML_val \<open>
    5.18    val s =
    5.19      Buffer.empty
    5.20      |> Buffer.add "digits: "
    5.21 @@ -1093,6 +1093,25 @@
    5.22      "The frumious Bandersnatch!"]);
    5.23  \<close>
    5.24  
    5.25 +text \<open>
    5.26 +  \medskip An alternative is to make a paragraph of freely-floating words as
    5.27 +  follows.
    5.28 +\<close>
    5.29 +
    5.30 +ML_command \<open>
    5.31 +  warning (Pretty.string_of (Pretty.para
    5.32 +    "Beware the Jabberwock, my son! \
    5.33 +    \The jaws that bite, the claws that catch! \
    5.34 +    \Beware the Jubjub Bird, and shun \
    5.35 +    \The frumious Bandersnatch!"))
    5.36 +\<close>
    5.37 +
    5.38 +text \<open>
    5.39 +  This has advantages with variable window / popup sizes, but might make it
    5.40 +  harder to search for message content systematically, e.g.\ by other tools or
    5.41 +  by humans expecting the ``verse'' of a formal message in a fixed layout.
    5.42 +\<close>
    5.43 +
    5.44  
    5.45  section \<open>Exceptions \label{sec:exceptions}\<close>
    5.46  
    5.47 @@ -1551,7 +1570,7 @@
    5.48    prevented.
    5.49  \<close>
    5.50  
    5.51 -ML \<open>
    5.52 +ML_val \<open>
    5.53    val items = [1, 2, 3, 4, 5, 6, 7, 8, 9, 10];
    5.54  
    5.55    val list1 = fold cons items [];
    5.56 @@ -1564,7 +1583,7 @@
    5.57  text \<open>The subsequent example demonstrates how to \emph{merge} two
    5.58    lists in a natural way.\<close>
    5.59  
    5.60 -ML \<open>
    5.61 +ML_val \<open>
    5.62    fun merge_lists eq (xs, ys) = fold_rev (insert eq) ys xs;
    5.63  \<close>
    5.64  
    5.65 @@ -1817,7 +1836,7 @@
    5.66    temporary file names.
    5.67  \<close>
    5.68  
    5.69 -ML \<open>
    5.70 +ML_val \<open>
    5.71    val tmp1 = File.tmp_path (Path.basic ("foo" ^ serial_string ()));
    5.72    val tmp2 = File.tmp_path (Path.basic ("foo" ^ serial_string ()));
    5.73    @{assert} (tmp1 <> tmp2);
    5.74 @@ -1878,7 +1897,7 @@
    5.75    positive integers that are unique over the runtime of the Isabelle
    5.76    process:\<close>
    5.77  
    5.78 -ML \<open>
    5.79 +ML_val \<open>
    5.80    local
    5.81      val counter = Synchronized.var "counter" 0;
    5.82    in
    5.83 @@ -1888,9 +1907,7 @@
    5.84            let val j = i + 1
    5.85            in SOME (j, j) end);
    5.86    end;
    5.87 -\<close>
    5.88 -
    5.89 -ML \<open>
    5.90 +
    5.91    val a = next ();
    5.92    val b = next ();
    5.93    @{assert} (a <> b);
     6.1 --- a/src/Doc/Implementation/Prelim.thy	Wed Apr 01 19:17:41 2015 +0200
     6.2 +++ b/src/Doc/Implementation/Prelim.thy	Wed Apr 01 22:40:41 2015 +0200
     6.3 @@ -501,6 +501,9 @@
     6.4    value can be modified within Isar text like this:
     6.5  \<close>
     6.6  
     6.7 +experiment
     6.8 +begin
     6.9 +
    6.10  declare [[show_types = false]]
    6.11    -- \<open>declaration within (local) theory context\<close>
    6.12  
    6.13 @@ -516,6 +519,8 @@
    6.14      ..
    6.15  end
    6.16  
    6.17 +end
    6.18 +
    6.19  text \<open>Configuration options that are not set explicitly hold a
    6.20    default value that can depend on the application context.  This
    6.21    allows to retrieve the value from another slot within the context,
    6.22 @@ -720,7 +725,7 @@
    6.23  text %mlex \<open>The following simple examples demonstrate how to produce
    6.24    fresh names from the initial @{ML Name.context}.\<close>
    6.25  
    6.26 -ML \<open>
    6.27 +ML_val \<open>
    6.28    val list1 = Name.invent Name.context "a" 5;
    6.29    @{assert} (list1 = ["a", "b", "c", "d", "e"]);
    6.30  
    6.31 @@ -732,10 +737,10 @@
    6.32  text \<open>\medskip The same works relatively to the formal context as
    6.33    follows.\<close>
    6.34  
    6.35 -locale ex = fixes a b c :: 'a
    6.36 +experiment fixes a b c :: 'a
    6.37  begin
    6.38  
    6.39 -ML \<open>
    6.40 +ML_val \<open>
    6.41    val names = Variable.names_of @{context};
    6.42  
    6.43    val list1 = Name.invent names "a" 5;
    6.44 @@ -1043,7 +1048,7 @@
    6.45    concrete binding inlined into the text:
    6.46  \<close>
    6.47  
    6.48 -ML \<open>Binding.pos_of @{binding here}\<close>
    6.49 +ML_val \<open>Binding.pos_of @{binding here}\<close>
    6.50  
    6.51  text \<open>\medskip That position can be also printed in a message as
    6.52    follows:\<close>
     7.1 --- a/src/Doc/Implementation/Proof.thy	Wed Apr 01 19:17:41 2015 +0200
     7.2 +++ b/src/Doc/Implementation/Proof.thy	Wed Apr 01 22:40:41 2015 +0200
     7.3 @@ -162,7 +162,7 @@
     7.4  text %mlex \<open>The following example shows how to work with fixed term
     7.5    and type parameters and with type-inference.\<close>
     7.6  
     7.7 -ML \<open>
     7.8 +ML_val \<open>
     7.9    (*static compile-time context -- for testing only*)
    7.10    val ctxt0 = @{context};
    7.11  
    7.12 @@ -188,7 +188,7 @@
    7.13    Alternatively, fixed parameters can be renamed explicitly as
    7.14    follows:\<close>
    7.15  
    7.16 -ML \<open>
    7.17 +ML_val \<open>
    7.18    val ctxt0 = @{context};
    7.19    val ([x1, x2, x3], ctxt1) =
    7.20      ctxt0 |> Variable.variant_fixes ["x", "x", "x"];
    7.21 @@ -325,7 +325,7 @@
    7.22    here for testing purposes.
    7.23  \<close>
    7.24  
    7.25 -ML \<open>
    7.26 +ML_val \<open>
    7.27    (*static compile-time context -- for testing only*)
    7.28    val ctxt0 = @{context};
    7.29  
     8.1 --- a/src/Doc/Implementation/Tactic.thy	Wed Apr 01 19:17:41 2015 +0200
     8.2 +++ b/src/Doc/Implementation/Tactic.thy	Wed Apr 01 22:40:41 2015 +0200
     8.3 @@ -709,7 +709,7 @@
     8.4    \end{warn}
     8.5  \<close>
     8.6  
     8.7 -ML \<open>
     8.8 +ML_val \<open>
     8.9    (*BAD -- does not terminate!*)
    8.10    fun REPEAT tac = (tac THEN REPEAT tac) ORELSE all_tac;
    8.11  \<close>
     9.1 --- a/src/Doc/Isar_Ref/Spec.thy	Wed Apr 01 19:17:41 2015 +0200
     9.2 +++ b/src/Doc/Isar_Ref/Spec.thy	Wed Apr 01 22:40:41 2015 +0200
     9.3 @@ -501,6 +501,7 @@
     9.4  text \<open>
     9.5    \begin{matharray}{rcl}
     9.6      @{command_def "locale"} & : & @{text "theory \<rightarrow> local_theory"} \\
     9.7 +    @{command_def "experiment"} & : & @{text "theory \<rightarrow> local_theory"} \\
     9.8      @{command_def "print_locale"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
     9.9      @{command_def "print_locales"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
    9.10      @{command_def "locale_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
    9.11 @@ -513,6 +514,8 @@
    9.12    @{rail \<open>
    9.13      @@{command locale} @{syntax name} ('=' @{syntax locale})? @'begin'?
    9.14      ;
    9.15 +    @@{command experiment} (@{syntax context_elem}*) @'begin'
    9.16 +    ;
    9.17      @@{command print_locale} '!'? @{syntax nameref}
    9.18      ;
    9.19      @{syntax_def locale}: @{syntax context_elem}+ |
    9.20 @@ -610,7 +613,12 @@
    9.21    @{text "\<Longrightarrow>"} by @{text "\<longrightarrow>"} in HOL; see also
    9.22    \secref{sec:object-logic}).  Separate introduction rules @{text
    9.23    loc_axioms.intro} and @{text loc.intro} are provided as well.
    9.24 -  
    9.25 +
    9.26 +  \item @{command experiment}~@{text exprs}~@{keyword "begin"} opens an
    9.27 +  anonymous locale context with private naming policy. Specifications in its
    9.28 +  body are inaccessible from outside. This is useful to perform experiments,
    9.29 +  without polluting the name space.
    9.30 +
    9.31    \item @{command "print_locale"}~@{text "locale"} prints the
    9.32    contents of the named locale.  The command omits @{element "notes"}
    9.33    elements by default.  Use @{command "print_locale"}@{text "!"} to
    10.1 --- a/src/Doc/System/Sessions.thy	Wed Apr 01 19:17:41 2015 +0200
    10.2 +++ b/src/Doc/System/Sessions.thy	Wed Apr 01 22:40:41 2015 +0200
    10.3 @@ -284,11 +284,13 @@
    10.4      -d DIR       include session directory
    10.5      -g NAME      select session group NAME
    10.6      -j INT       maximum number of parallel jobs (default 1)
    10.7 +    -k KEYWORD   check theory sources for conflicts with proposed keywords
    10.8      -l           list session source files
    10.9      -n           no build -- test dependencies only
   10.10      -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
   10.11      -s           system build mode: produce output in ISABELLE_HOME
   10.12      -v           verbose
   10.13 +    -x SESSION   exclude SESSION and all its descendants
   10.14  
   10.15    Build and manage Isabelle sessions, depending on implicit
   10.16    ISABELLE_BUILD_OPTIONS="..."
   10.17 @@ -321,6 +323,10 @@
   10.18    The build tool takes session dependencies into account: the set of
   10.19    selected sessions is completed by including all ancestors.
   10.20  
   10.21 +  \medskip One or more options @{verbatim "-x"}~@{text SESSION} specify
   10.22 +  sessions to be excluded. All descendents of excluded sessions are removed
   10.23 +  from the selection as specified above.
   10.24 +
   10.25    \medskip Option @{verbatim "-R"} reverses the selection in the sense
   10.26    that it refers to its requirements: all ancestor sessions excluding
   10.27    the original selection.  This allows to prepare the stage for some
   10.28 @@ -369,7 +375,12 @@
   10.29    \medskip Option @{verbatim "-v"} increases the general level of
   10.30    verbosity.  Option @{verbatim "-l"} lists the source files that
   10.31    contribute to a session.
   10.32 -\<close>
   10.33 +
   10.34 +  \medskip Option @{verbatim "-k"} specifies a newly proposed keyword for
   10.35 +  outer syntax (multiple uses allowed). The theory sources are checked for
   10.36 +  conflicts wrt.\ this hypothetical change of syntax, e.g.\ to reveal
   10.37 +  occurrences of identifiers that need to be quoted.\<close>
   10.38 +
   10.39  
   10.40  subsubsection \<open>Examples\<close>
   10.41  
    11.1 --- a/src/FOL/ex/Locale_Test/Locale_Test1.thy	Wed Apr 01 19:17:41 2015 +0200
    11.2 +++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy	Wed Apr 01 22:40:41 2015 +0200
    11.3 @@ -775,7 +775,7 @@
    11.4  
    11.5  locale container
    11.6  begin
    11.7 -interpretation private!: roundup True by unfold_locales rule
    11.8 +interpretation "private"!: roundup True by unfold_locales rule
    11.9  lemmas true_copy = private.true
   11.10  end
   11.11  
    12.1 --- a/src/HOL/Bali/WellForm.thy	Wed Apr 01 19:17:41 2015 +0200
    12.2 +++ b/src/HOL/Bali/WellForm.thy	Wed Apr 01 22:40:41 2015 +0200
    12.3 @@ -1979,7 +1979,7 @@
    12.4  
    12.5  lemma dynmethd_Object:
    12.6    assumes statM: "methd G Object sig = Some statM" and
    12.7 -        private: "accmodi statM = Private" and 
    12.8 +        "private": "accmodi statM = Private" and 
    12.9         is_cls_C: "is_class G C" and
   12.10               wf: "wf_prog G"
   12.11    shows "dynmethd G Object C sig = Some statM"
   12.12 @@ -1992,13 +1992,13 @@
   12.13    from wf 
   12.14    have is_cls_Obj: "is_class G Object" 
   12.15      by simp
   12.16 -  from statM subclseq is_cls_Obj ws private
   12.17 +  from statM subclseq is_cls_Obj ws "private"
   12.18    show ?thesis
   12.19    proof (cases rule: dynmethd_cases)
   12.20      case Static then show ?thesis .
   12.21    next
   12.22      case Overrides 
   12.23 -    with private show ?thesis 
   12.24 +    with "private" show ?thesis 
   12.25        by (auto dest: no_Private_override)
   12.26    qed
   12.27  qed
    13.1 --- a/src/HOL/Library/Code_Test.thy	Wed Apr 01 19:17:41 2015 +0200
    13.2 +++ b/src/HOL/Library/Code_Test.thy	Wed Apr 01 22:40:41 2015 +0200
    13.3 @@ -64,7 +64,7 @@
    13.4  by(cases x y rule: xml_tree.exhaust[case_product xml_tree.exhaust])(simp)
    13.5  
    13.6  context begin
    13.7 -local_setup {* Local_Theory.map_naming (Name_Space.mandatory_path "xml") *}
    13.8 +local_setup {* Local_Theory.map_background_naming (Name_Space.mandatory_path "xml") *}
    13.9  
   13.10  type_synonym attributes = "(String.literal \<times> String.literal) list"
   13.11  type_synonym body = "xml_tree list"
    14.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Wed Apr 01 19:17:41 2015 +0200
    14.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Wed Apr 01 22:40:41 2015 +0200
    14.3 @@ -529,7 +529,7 @@
    14.4  
    14.5      val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy4) =
    14.6        thy3
    14.7 -      |> Sign.map_naming Name_Space.concealed
    14.8 +      |> Sign.concealed
    14.9        |> Inductive.add_inductive_global
   14.10            {quiet_mode = false, verbose = false, alt_name = Binding.name big_rep_name,
   14.11             coind = false, no_elim = true, no_ind = false, skip_mono = true}
   14.12 @@ -1505,7 +1505,7 @@
   14.13  
   14.14      val ({intrs = rec_intrs, elims = rec_elims, raw_induct = rec_induct, ...}, thy11) =
   14.15        thy10
   14.16 -      |> Sign.map_naming Name_Space.concealed
   14.17 +      |> Sign.concealed
   14.18        |> Inductive.add_inductive_global
   14.19            {quiet_mode = #quiet config, verbose = false, alt_name = Binding.name big_rec_name,
   14.20             coind = false, no_elim = false, no_ind = false, skip_mono = true}
    15.1 --- a/src/HOL/Product_Type.thy	Wed Apr 01 19:17:41 2015 +0200
    15.2 +++ b/src/HOL/Product_Type.thy	Wed Apr 01 22:40:41 2015 +0200
    15.3 @@ -988,7 +988,7 @@
    15.4  context
    15.5  begin
    15.6  
    15.7 -local_setup {* Local_Theory.map_naming (Name_Space.mandatory_path "prod") *}
    15.8 +local_setup {* Local_Theory.map_background_naming (Name_Space.mandatory_path "prod") *}
    15.9  
   15.10  definition swap :: "'a \<times> 'b \<Rightarrow> 'b \<times> 'a"
   15.11  where
    16.1 --- a/src/HOL/ROOT	Wed Apr 01 19:17:41 2015 +0200
    16.2 +++ b/src/HOL/ROOT	Wed Apr 01 22:40:41 2015 +0200
    16.3 @@ -706,7 +706,7 @@
    16.4      "ex/Measure_Not_CCC"
    16.5    document_files "root.tex"
    16.6  
    16.7 -session "HOL-Nominal" (main) in Nominal = HOL +
    16.8 +session "HOL-Nominal" in Nominal = HOL +
    16.9    options [document = false]
   16.10    theories Nominal
   16.11  
    17.1 --- a/src/HOL/Statespace/state_space.ML	Wed Apr 01 19:17:41 2015 +0200
    17.2 +++ b/src/HOL/Statespace/state_space.ML	Wed Apr 01 22:40:41 2015 +0200
    17.3 @@ -173,7 +173,7 @@
    17.4  fun mk_free ctxt name =
    17.5    if Variable.is_fixed ctxt name orelse Variable.is_declared ctxt name
    17.6    then
    17.7 -    let val n' = Variable.intern_fixed ctxt name
    17.8 +    let val n' = Variable.intern_fixed ctxt name |> perhaps Long_Name.dest_hidden;
    17.9      in SOME (Free (n', Proof_Context.infer_type ctxt (n', dummyT))) end
   17.10    else NONE
   17.11  
    18.1 --- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Wed Apr 01 19:17:41 2015 +0200
    18.2 +++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Wed Apr 01 22:40:41 2015 +0200
    18.3 @@ -737,16 +737,17 @@
    18.4               bnd_def
    18.5  
    18.6      val thm =
    18.7 -      if Name_Space.defined_entry (Theory.axiom_space thy) def_name then
    18.8 -        Thm.axiom thy def_name
    18.9 -      else
   18.10 -        if is_none prob_name_opt then
   18.11 -          (*This mode is for testing, so we can be a bit
   18.12 -            looser with theories*)
   18.13 -          Thm.add_axiom_global (bnd_name, conclusion) thy
   18.14 -          |> fst |> snd
   18.15 -        else
   18.16 -          raise (NO_SKOLEM_DEF (def_name, bnd_name, conclusion))
   18.17 +      (case try (Thm.axiom thy) def_name of
   18.18 +        SOME thm => thm
   18.19 +      | NONE =>
   18.20 +          if is_none prob_name_opt then
   18.21 +            (*This mode is for testing, so we can be a bit
   18.22 +              looser with theories*)
   18.23 +            (* FIXME bad theory context!? *)
   18.24 +            Thm.add_axiom_global (bnd_name, conclusion) thy
   18.25 +            |> fst |> snd
   18.26 +          else
   18.27 +            raise (NO_SKOLEM_DEF (def_name, bnd_name, conclusion)))
   18.28    in
   18.29      rtac (Drule.export_without_context thm) i st
   18.30    end
    19.1 --- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed Apr 01 19:17:41 2015 +0200
    19.2 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed Apr 01 22:40:41 2015 +0200
    19.3 @@ -396,9 +396,8 @@
    19.4  fun make_class clas = class_prefix ^ ascii_of clas
    19.5  
    19.6  fun new_skolem_var_name_of_const s =
    19.7 -  let val ss = s |> space_explode Long_Name.separator in
    19.8 -    nth ss (length ss - 2)
    19.9 -  end
   19.10 +  let val ss = Long_Name.explode s
   19.11 +  in nth ss (length ss - 2) end
   19.12  
   19.13  (* These are ignored anyway by the relevance filter (unless they appear in
   19.14     higher-order places) but not by the monomorphizer. *)
    20.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Apr 01 19:17:41 2015 +0200
    20.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Apr 01 22:40:41 2015 +0200
    20.3 @@ -414,9 +414,8 @@
    20.4      val ps = map (`Long_Name.base_name) names;
    20.5      val dups = Library.duplicates (op =) (map fst ps);
    20.6      fun underscore s =
    20.7 -      let val ss = space_explode Long_Name.separator s in
    20.8 -        space_implode "_" (drop (length ss - 2) ss)
    20.9 -      end;
   20.10 +      let val ss = Long_Name.explode s
   20.11 +      in space_implode "_" (drop (length ss - 2) ss) end;
   20.12    in
   20.13      map (fn (base, full) => if member (op =) dups base then underscore full else base) ps
   20.14      |> Name.variant_list []
    21.1 --- a/src/HOL/Tools/BNF/bnf_util.ML	Wed Apr 01 19:17:41 2015 +0200
    21.2 +++ b/src/HOL/Tools/BNF/bnf_util.ML	Wed Apr 01 22:40:41 2015 +0200
    21.3 @@ -145,9 +145,9 @@
    21.4      val b' = fold_rev Binding.prefix_name (map (suffix "_" o fst) (Binding.path_of b)) b;
    21.5      val ((name, info), (lthy, lthy_old)) =
    21.6        lthy
    21.7 -      |> Local_Theory.concealed
    21.8 +      |> Proof_Context.concealed
    21.9        |> Typedef.add_typedef true (b', Ts, mx) set opt_morphs tac
   21.10 -      ||> Local_Theory.restore_naming lthy
   21.11 +      ||> Proof_Context.restore_naming lthy
   21.12        ||> `Local_Theory.restore;
   21.13      val phi = Proof_Context.export_morphism lthy_old lthy;
   21.14    in
    22.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Wed Apr 01 19:17:41 2015 +0200
    22.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Wed Apr 01 22:40:41 2015 +0200
    22.3 @@ -231,7 +231,7 @@
    22.4    | name_noted_thms qualifier base ((local_name, thms) :: noted) =
    22.5      if Long_Name.base_name local_name = base then
    22.6        (local_name,
    22.7 -       map_index (uncurry (fn j => Thm.name_derivation (qualifier ^ Long_Name.separator ^ base ^
    22.8 +       map_index (uncurry (fn j => Thm.name_derivation (Long_Name.append qualifier base ^
    22.9           (if can the_single thms then "" else "_" ^ string_of_int (j + 1))))) thms) :: noted
   22.10      else
   22.11        ((local_name, thms) :: name_noted_thms qualifier base noted);
    23.1 --- a/src/HOL/Tools/Function/function_core.ML	Wed Apr 01 19:17:41 2015 +0200
    23.2 +++ b/src/HOL/Tools/Function/function_core.ML	Wed Apr 01 22:40:41 2015 +0200
    23.3 @@ -445,7 +445,7 @@
    23.4    let
    23.5      val ({intrs = intrs_gen, elims = [elim_gen], preds = [ Rdef ], induct, ...}, lthy) =
    23.6        lthy
    23.7 -      |> Local_Theory.concealed
    23.8 +      |> Proof_Context.concealed
    23.9        |> Inductive.add_inductive_i
   23.10            {quiet_mode = true,
   23.11              verbose = ! trace,
   23.12 @@ -458,7 +458,7 @@
   23.13            [] (* no parameters *)
   23.14            (map (fn t => (Attrib.empty_binding, t)) intrs) (* intro rules *)
   23.15            [] (* no special monos *)
   23.16 -      ||> Local_Theory.restore_naming lthy
   23.17 +      ||> Proof_Context.restore_naming lthy
   23.18  
   23.19      fun requantify orig_intro thm =
   23.20        let
    24.1 --- a/src/HOL/Tools/Metis/metis_generate.ML	Wed Apr 01 19:17:41 2015 +0200
    24.2 +++ b/src/HOL/Tools/Metis/metis_generate.ML	Wed Apr 01 22:40:41 2015 +0200
    24.3 @@ -66,8 +66,7 @@
    24.4          else metis_ad_hoc_type_tag, true))]
    24.5  
    24.6  fun old_skolem_const_name i j num_T_args =
    24.7 -  old_skolem_const_prefix ^ Long_Name.separator ^
    24.8 -  (space_implode Long_Name.separator (map string_of_int [i, j, num_T_args]))
    24.9 +  Long_Name.implode (old_skolem_const_prefix :: map string_of_int [i, j, num_T_args])
   24.10  
   24.11  fun conceal_old_skolem_terms i old_skolems t =
   24.12    if exists_Const (curry (op =) @{const_name Meson.skolem} o fst) t then
    25.1 --- a/src/HOL/Tools/Old_Datatype/old_datatype.ML	Wed Apr 01 19:17:41 2015 +0200
    25.2 +++ b/src/HOL/Tools/Old_Datatype/old_datatype.ML	Wed Apr 01 22:40:41 2015 +0200
    25.3 @@ -172,7 +172,7 @@
    25.4  
    25.5      val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy2) =
    25.6        thy1
    25.7 -      |> Sign.map_naming Name_Space.concealed
    25.8 +      |> Sign.concealed
    25.9        |> Inductive.add_inductive_global
   25.10            {quiet_mode = #quiet config, verbose = false, alt_name = Binding.name big_rec_name,
   25.11             coind = false, no_elim = true, no_ind = false, skip_mono = true}
    26.1 --- a/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML	Wed Apr 01 19:17:41 2015 +0200
    26.2 +++ b/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML	Wed Apr 01 22:40:41 2015 +0200
    26.3 @@ -146,7 +146,7 @@
    26.4  
    26.5      val ({intrs = rec_intrs, elims = rec_elims, ...}, thy1) =
    26.6        thy0
    26.7 -      |> Sign.map_naming Name_Space.concealed
    26.8 +      |> Sign.concealed
    26.9        |> Inductive.add_inductive_global
   26.10            {quiet_mode = #quiet config, verbose = false, alt_name = Binding.name big_rec_name',
   26.11              coind = false, no_elim = false, no_ind = true, skip_mono = true}
    27.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Apr 01 19:17:41 2015 +0200
    27.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Apr 01 22:40:41 2015 +0200
    27.3 @@ -476,7 +476,7 @@
    27.4      fun add_facts global foldx facts =
    27.5        foldx (fn (name0, ths) => fn accum =>
    27.6          if name0 <> "" andalso
    27.7 -           (Long_Name.is_hidden (Facts.intern facts name0) orelse
    27.8 +           (is_some (Long_Name.dest_hidden (Facts.intern facts name0)) orelse
    27.9              ((Facts.is_concealed facts name0 orelse
   27.10                (not generous andalso is_blacklisted_or_something name0)) andalso
   27.11               forall (not o member Thm.eq_thm_prop add_ths) ths)) then
    28.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Wed Apr 01 19:17:41 2015 +0200
    28.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Wed Apr 01 22:40:41 2015 +0200
    28.3 @@ -737,8 +737,6 @@
    28.4  
    28.5  (*** Isabelle helpers ***)
    28.6  
    28.7 -val local_prefix = "local" ^ Long_Name.separator
    28.8 -
    28.9  fun elided_backquote_thm threshold th =
   28.10    elide_string threshold (backquote_thm (Proof_Context.init_global (Thm.theory_of_thm th)) th)
   28.11  
   28.12 @@ -748,10 +746,8 @@
   28.13    if Thm.has_name_hint th then
   28.14      let val hint = Thm.get_name_hint th in
   28.15        (* There must be a better way to detect local facts. *)
   28.16 -      (case try (unprefix local_prefix) hint of
   28.17 -        SOME suf =>
   28.18 -        thy_name_of_thm th ^ Long_Name.separator ^ suf ^ Long_Name.separator ^
   28.19 -        elided_backquote_thm 50 th
   28.20 +      (case Long_Name.dest_local hint of
   28.21 +        SOME suf => Long_Name.implode [thy_name_of_thm th, suf, elided_backquote_thm 50 th]
   28.22        | NONE => hint)
   28.23      end
   28.24    else
   28.25 @@ -886,7 +882,7 @@
   28.26        | pattify_term _ _ (Free (s, T)) =
   28.27          maybe_singleton_str pat_var_prefix (crude_str_of_typ T)
   28.28          |> (if member (op =) fixes s then
   28.29 -              cons (free_feature_of (massage_long_name (thy_name ^ Long_Name.separator ^ s)))
   28.30 +              cons (free_feature_of (massage_long_name (Long_Name.append thy_name s)))
   28.31              else
   28.32                I)
   28.33        | pattify_term _ _ (Var (_, T)) = maybe_singleton_str pat_var_prefix (crude_str_of_typ T)
    29.1 --- a/src/HOL/Tools/inductive.ML	Wed Apr 01 19:17:41 2015 +0200
    29.2 +++ b/src/HOL/Tools/inductive.ML	Wed Apr 01 22:40:41 2015 +0200
    29.3 @@ -843,13 +843,13 @@
    29.4  
    29.5      val is_auxiliary = length cs >= 2; 
    29.6      val ((rec_const, (_, fp_def)), lthy') = lthy
    29.7 -      |> is_auxiliary ? Local_Theory.concealed
    29.8 +      |> is_auxiliary ? Proof_Context.concealed
    29.9        |> Local_Theory.define
   29.10          ((rec_name, case cnames_syn of [(_, syn)] => syn | _ => NoSyn),
   29.11           ((Binding.concealed (Thm.def_binding rec_name), @{attributes [nitpick_unfold]}),
   29.12             fold_rev lambda params
   29.13               (Const (fp_name, (predT --> predT) --> predT) $ fp_fun)))
   29.14 -      ||> is_auxiliary ? Local_Theory.restore_naming lthy;
   29.15 +      ||> Proof_Context.restore_naming lthy;
   29.16      val fp_def' =
   29.17        Simplifier.rewrite (put_simpset HOL_basic_ss lthy' addsimps [fp_def])
   29.18          (Thm.cterm_of lthy' (list_comb (rec_const, params)));
    30.1 --- a/src/HOL/Tools/inductive_set.ML	Wed Apr 01 19:17:41 2015 +0200
    30.2 +++ b/src/HOL/Tools/inductive_set.ML	Wed Apr 01 22:40:41 2015 +0200
    30.3 @@ -488,13 +488,13 @@
    30.4  
    30.5      (* define inductive sets using previously defined predicates *)
    30.6      val (defs, lthy2) = lthy1
    30.7 -      |> Local_Theory.concealed  (* FIXME ?? *)
    30.8 +      |> Proof_Context.concealed  (* FIXME ?? *)
    30.9        |> fold_map Local_Theory.define
   30.10          (map (fn (((c, syn), (fs, U, _)), p) => ((c, syn), ((Thm.def_binding c, []),
   30.11             fold_rev lambda params (HOLogic.Collect_const U $
   30.12               HOLogic.mk_psplits fs U HOLogic.boolT (list_comb (p, params3))))))
   30.13             (cnames_syn ~~ cs_info ~~ preds))
   30.14 -      ||> Local_Theory.restore_naming lthy1;
   30.15 +      ||> Proof_Context.restore_naming lthy1;
   30.16  
   30.17      (* prove theorems for converting predicate to set notation *)
   30.18      val lthy3 = fold
    31.1 --- a/src/HOL/Tools/typedef.ML	Wed Apr 01 19:17:41 2015 +0200
    31.2 +++ b/src/HOL/Tools/typedef.ML	Wed Apr 01 22:40:41 2015 +0200
    31.3 @@ -81,10 +81,10 @@
    31.4    Typedef_Plugin.interpretation typedef_plugin
    31.5      (fn name => fn lthy =>
    31.6        lthy
    31.7 -      |> Local_Theory.map_naming
    31.8 +      |> Local_Theory.map_background_naming
    31.9            (Name_Space.root_path #> Name_Space.add_path (Long_Name.qualifier name))
   31.10        |> f name
   31.11 -      |> Local_Theory.restore_naming lthy);
   31.12 +      |> Local_Theory.restore_background_naming lthy);
   31.13  
   31.14  
   31.15  (* primitive typedef axiomatization -- for fresh typedecl *)
    32.1 --- a/src/Pure/General/binding.ML	Wed Apr 01 19:17:41 2015 +0200
    32.2 +++ b/src/Pure/General/binding.ML	Wed Apr 01 22:40:41 2015 +0200
    32.3 @@ -9,8 +9,9 @@
    32.4  
    32.5  signature BINDING =
    32.6  sig
    32.7 +  eqtype scope
    32.8 +  val new_scope: unit -> scope
    32.9    eqtype binding
   32.10 -  val dest: binding -> {private: bool, concealed: bool, path: (string * bool) list, name: bstring}
   32.11    val path_of: binding -> (string * bool) list
   32.12    val make: bstring * Position.T -> binding
   32.13    val pos_of: binding -> Position.T
   32.14 @@ -29,13 +30,16 @@
   32.15    val prefix_of: binding -> (string * bool) list
   32.16    val map_prefix: ((string * bool) list -> (string * bool) list) -> binding -> binding
   32.17    val prefix: bool -> string -> binding -> binding
   32.18 -  val private: binding -> binding
   32.19 +  val private: scope -> binding -> binding
   32.20 +  val private_default: scope option -> binding -> binding
   32.21    val concealed: binding -> binding
   32.22    val pretty: binding -> Pretty.T
   32.23    val print: binding -> string
   32.24    val pp: binding -> Pretty.T
   32.25    val bad: binding -> string
   32.26    val check: binding -> unit
   32.27 +  val name_spec: scope list -> (string * bool) list -> binding ->
   32.28 +    {accessible: bool, concealed: bool, spec: (string * bool) list}
   32.29  end;
   32.30  
   32.31  structure Binding: BINDING =
   32.32 @@ -43,10 +47,17 @@
   32.33  
   32.34  (** representation **)
   32.35  
   32.36 -(* datatype *)
   32.37 +(* scope of private entries *)
   32.38 +
   32.39 +datatype scope = Scope of serial;
   32.40 +
   32.41 +fun new_scope () = Scope (serial ());
   32.42 +
   32.43 +
   32.44 +(* binding *)
   32.45  
   32.46  datatype binding = Binding of
   32.47 - {private: bool,                    (*entry is strictly private -- no name space accesses*)
   32.48 + {private: scope option,            (*entry is strictly private within its scope*)
   32.49    concealed: bool,                  (*entry is for foundational purposes -- please ignore*)
   32.50    prefix: (string * bool) list,     (*system prefix*)
   32.51    qualifier: (string * bool) list,  (*user qualifier*)
   32.52 @@ -60,10 +71,7 @@
   32.53  fun map_binding f (Binding {private, concealed, prefix, qualifier, name, pos}) =
   32.54    make_binding (f (private, concealed, prefix, qualifier, name, pos));
   32.55  
   32.56 -fun dest (Binding {private, concealed, prefix, qualifier, name, ...}) =
   32.57 -  {private = private, concealed = concealed, path = prefix @ qualifier, name = name};
   32.58 -
   32.59 -val path_of = #path o dest;
   32.60 +fun path_of (Binding {prefix, qualifier, ...}) = prefix @ qualifier;
   32.61  
   32.62  
   32.63  
   32.64 @@ -71,7 +79,7 @@
   32.65  
   32.66  (* name and position *)
   32.67  
   32.68 -fun make (name, pos) = make_binding (false, false, [], [], name, pos);
   32.69 +fun make (name, pos) = make_binding (NONE, false, [], [], name, pos);
   32.70  
   32.71  fun pos_of (Binding {pos, ...}) = pos;
   32.72  fun set_pos pos =
   32.73 @@ -109,7 +117,7 @@
   32.74  fun qualified_name "" = empty
   32.75    | qualified_name s =
   32.76        let val (qualifier, name) = split_last (Long_Name.explode s)
   32.77 -      in make_binding (false, false, [], map (rpair false) qualifier, name, Position.none) end;
   32.78 +      in make_binding (NONE, false, [], map (rpair false) qualifier, name, Position.none) end;
   32.79  
   32.80  
   32.81  (* system prefix *)
   32.82 @@ -126,9 +134,13 @@
   32.83  
   32.84  (* visibility flags *)
   32.85  
   32.86 -val private =
   32.87 +fun private scope =
   32.88    map_binding (fn (_, concealed, prefix, qualifier, name, pos) =>
   32.89 -    (true, concealed, prefix, qualifier, name, pos));
   32.90 +    (SOME scope, concealed, prefix, qualifier, name, pos));
   32.91 +
   32.92 +fun private_default private' =
   32.93 +  map_binding (fn (private, concealed, prefix, qualifier, name, pos) =>
   32.94 +    (if is_some private then private else private', concealed, prefix, qualifier, name, pos));
   32.95  
   32.96  val concealed =
   32.97    map_binding (fn (private, _, prefix, qualifier, name, pos) =>
   32.98 @@ -157,6 +169,31 @@
   32.99    if Symbol_Pos.is_identifier (name_of binding) then ()
  32.100    else legacy_feature (bad binding);
  32.101  
  32.102 +
  32.103 +
  32.104 +(** resulting name_spec **)
  32.105 +
  32.106 +val bad_specs = ["", "??", "__"];
  32.107 +
  32.108 +fun name_spec scopes path binding =
  32.109 +  let
  32.110 +    val Binding {private, concealed, prefix, qualifier, name, ...} = binding;
  32.111 +    val _ = Long_Name.is_qualified name andalso error (bad binding);
  32.112 +
  32.113 +    val accessible =
  32.114 +      (case private of
  32.115 +        NONE => true
  32.116 +      | SOME scope => member (op =) scopes scope);
  32.117 +
  32.118 +    val spec1 =
  32.119 +      maps (fn (a, b) => map (rpair b) (Long_Name.explode a)) (path @ prefix @ qualifier);
  32.120 +    val spec2 = if name = "" then [] else [(name, true)];
  32.121 +    val spec = spec1 @ spec2;
  32.122 +    val _ =
  32.123 +      exists (fn (a, _) => member (op =) bad_specs a orelse exists_string (fn s => s = "\"") a) spec
  32.124 +      andalso error (bad binding);
  32.125 +  in {accessible = accessible, concealed = concealed, spec = if null spec2 then [] else spec} end;
  32.126 +
  32.127  end;
  32.128  
  32.129  type binding = Binding.binding;
    33.1 --- a/src/Pure/General/long_name.ML	Wed Apr 01 19:17:41 2015 +0200
    33.2 +++ b/src/Pure/General/long_name.ML	Wed Apr 01 22:40:41 2015 +0200
    33.3 @@ -9,9 +9,9 @@
    33.4    val separator: string
    33.5    val is_qualified: string -> bool
    33.6    val hidden: string -> string
    33.7 -  val is_hidden: string -> bool
    33.8 +  val dest_hidden: string -> string option
    33.9    val localN: string
   33.10 -  val is_local: string -> bool
   33.11 +  val dest_local: string -> string option
   33.12    val implode: string list -> string
   33.13    val explode: string -> string list
   33.14    val append: string -> string -> string
   33.15 @@ -29,11 +29,11 @@
   33.16  
   33.17  val is_qualified = exists_string (fn s => s = separator);
   33.18  
   33.19 -fun hidden name = "??." ^ name;
   33.20 -val is_hidden = String.isPrefix "??.";
   33.21 +val hidden = prefix "??.";
   33.22 +val dest_hidden = try (unprefix "??.");
   33.23  
   33.24  val localN = "local";
   33.25 -val is_local = String.isPrefix "local.";
   33.26 +val dest_local = try (unprefix "local.");
   33.27  
   33.28  val implode = space_implode separator;
   33.29  val explode = space_explode separator;
    34.1 --- a/src/Pure/General/name_space.ML	Wed Apr 01 19:17:41 2015 +0200
    34.2 +++ b/src/Pure/General/name_space.ML	Wed Apr 01 22:40:41 2015 +0200
    34.3 @@ -12,11 +12,10 @@
    34.4    type T
    34.5    val empty: string -> T
    34.6    val kind_of: T -> string
    34.7 -  val defined_entry: T -> string -> bool
    34.8 +  val markup: T -> string -> Markup.T
    34.9    val the_entry: T -> string ->
   34.10      {concealed: bool, group: serial option, theory_name: string, pos: Position.T, serial: serial}
   34.11    val entry_ord: T -> string * string -> order
   34.12 -  val markup: T -> string -> Markup.T
   34.13    val is_concealed: T -> string -> bool
   34.14    val intern: T -> xstring -> string
   34.15    val names_long_raw: Config.raw
   34.16 @@ -33,7 +32,9 @@
   34.17    val completion: Context.generic -> T -> xstring * Position.T -> Completion.T
   34.18    val merge: T * T -> T
   34.19    type naming
   34.20 -  val private: naming -> naming
   34.21 +  val get_scope: naming -> Binding.scope option
   34.22 +  val new_scope: naming -> Binding.scope * naming
   34.23 +  val private: Binding.scope -> naming -> naming
   34.24    val concealed: naming -> naming
   34.25    val get_group: naming -> serial option
   34.26    val set_group: serial option -> naming -> naming
   34.27 @@ -47,6 +48,7 @@
   34.28    val qualified_path: bool -> binding -> naming -> naming
   34.29    val global_naming: naming
   34.30    val local_naming: naming
   34.31 +  val transform_naming: naming -> naming -> naming
   34.32    val transform_binding: naming -> binding -> binding
   34.33    val full_name: naming -> binding -> string
   34.34    val base_name: binding -> string
   34.35 @@ -62,6 +64,8 @@
   34.36    val check_reports: Context.generic -> 'a table ->
   34.37      xstring * Position.T list -> (string * Position.report list) * 'a
   34.38    val check: Context.generic -> 'a table -> xstring * Position.T -> string * 'a
   34.39 +  val defined: 'a table -> string -> bool
   34.40 +  val lookup: 'a table -> string -> 'a option
   34.41    val lookup_key: 'a table -> string -> (string * 'a) option
   34.42    val get: 'a table -> string -> 'a
   34.43    val define: Context.generic -> bool -> binding * 'a -> 'a table -> string * 'a table
   34.44 @@ -105,12 +109,10 @@
   34.45    error ("Duplicate " ^ plain_words kind ^ " declaration " ^
   34.46      print_entry_ref kind entry1 ^ " vs. " ^ print_entry_ref kind entry2 ^ Position.here pos);
   34.47  
   34.48 -fun undefined kind name = "Undefined " ^ plain_words kind ^ ": " ^ quote name;
   34.49 -
   34.50  
   34.51  (* internal names *)
   34.52  
   34.53 -type internals = (string list * string list) Change_Table.T;  (*xname -> visible, hidden*)
   34.54 +type internals = (string list * string list) Change_Table.T;
   34.55  
   34.56  fun map_internals f xname : internals -> internals =
   34.57    Change_Table.map_default (xname, ([], [])) f;
   34.58 @@ -119,14 +121,15 @@
   34.59  fun del_name_extra name =
   34.60    map_internals (apfst (fn [] => [] | x :: xs => x :: remove (op =) name xs));
   34.61  val add_name = map_internals o apfst o update (op =);
   34.62 -val add_name' = map_internals o apsnd o update (op =);
   34.63 +fun hide_name name = map_internals (apsnd (update (op =) name)) name;
   34.64  
   34.65  
   34.66  (* datatype T *)
   34.67  
   34.68  datatype T =
   34.69    Name_Space of
   34.70 -   {kind: string, internals: internals,
   34.71 +   {kind: string,
   34.72 +    internals: internals,  (*xname -> visible, hidden*)
   34.73      entries: (xstring list * entry) Change_Table.T};  (*name -> externals, entry*)
   34.74  
   34.75  fun make_name_space (kind, internals, entries) =
   34.76 @@ -146,36 +149,46 @@
   34.77  
   34.78  fun kind_of (Name_Space {kind, ...}) = kind;
   34.79  
   34.80 -fun defined_entry (Name_Space {entries, ...}) = Change_Table.defined entries;
   34.81 -
   34.82 -fun the_entry (Name_Space {kind, entries, ...}) name =
   34.83 -  (case Change_Table.lookup entries name of
   34.84 -    NONE => error (undefined kind name)
   34.85 -  | SOME (_, entry) => entry);
   34.86 -
   34.87 -fun entry_ord space = int_ord o apply2 (#serial o the_entry space);
   34.88 -
   34.89  fun markup (Name_Space {kind, entries, ...}) name =
   34.90    (case Change_Table.lookup entries name of
   34.91      NONE => Markup.intensify
   34.92    | SOME (_, entry) => entry_markup false kind (name, entry));
   34.93  
   34.94 +fun undefined (space as Name_Space {kind, entries, ...}) bad =
   34.95 +  let
   34.96 +    val (prfx, sfx) =
   34.97 +      (case Long_Name.dest_hidden bad of
   34.98 +        SOME name =>
   34.99 +          if Change_Table.defined entries name
  34.100 +          then ("Inaccessible", Markup.markup (markup space name) (quote name))
  34.101 +          else ("Undefined", quote name)
  34.102 +      | NONE => ("Undefined", quote bad));
  34.103 +  in prfx ^ " " ^ plain_words kind ^ ": " ^ sfx end;
  34.104 +
  34.105 +fun the_entry (space as Name_Space {entries, ...}) name =
  34.106 +  (case Change_Table.lookup entries name of
  34.107 +    NONE => error (undefined space name)
  34.108 +  | SOME (_, entry) => entry);
  34.109 +
  34.110 +fun entry_ord space = int_ord o apply2 (#serial o the_entry space);
  34.111 +
  34.112  fun is_concealed space name = #concealed (the_entry space name);
  34.113  
  34.114  
  34.115 -(* name accesses *)
  34.116 +(* intern *)
  34.117  
  34.118 -fun lookup (Name_Space {internals, ...}) xname =
  34.119 -  (case Change_Table.lookup internals xname of
  34.120 -    NONE => (xname, true)
  34.121 -  | SOME ([], []) => (xname, true)
  34.122 -  | SOME ([name], _) => (name, true)
  34.123 -  | SOME (name :: _, _) => (name, false)
  34.124 -  | SOME ([], name' :: _) => (Long_Name.hidden name', true));
  34.125 +fun intern' (Name_Space {internals, ...}) xname =
  34.126 +  (case the_default ([], []) (Change_Table.lookup internals xname) of
  34.127 +    ([name], _) => (name, true)
  34.128 +  | (name :: _, _) => (name, false)
  34.129 +  | ([], []) => (Long_Name.hidden xname, true)
  34.130 +  | ([], name' :: _) => (Long_Name.hidden name', true));
  34.131 +
  34.132 +val intern = #1 oo intern';
  34.133  
  34.134  fun get_accesses (Name_Space {entries, ...}) name =
  34.135    (case Change_Table.lookup entries name of
  34.136 -    NONE => [name]
  34.137 +    NONE => []
  34.138    | SOME (externals, _) => externals);
  34.139  
  34.140  fun valid_accesses (Name_Space {internals, ...}) name =
  34.141 @@ -183,11 +196,6 @@
  34.142      if not (null names) andalso hd names = name then cons xname else I) internals [];
  34.143  
  34.144  
  34.145 -(* intern *)
  34.146 -
  34.147 -fun intern space xname = #1 (lookup space xname);
  34.148 -
  34.149 -
  34.150  (* extern *)
  34.151  
  34.152  val names_long_raw = Config.declare_option ("names_long", @{here});
  34.153 @@ -206,7 +214,7 @@
  34.154      val names_unique = Config.get ctxt names_unique;
  34.155  
  34.156      fun valid require_unique xname =
  34.157 -      let val (name', is_unique) = lookup space xname
  34.158 +      let val (name', is_unique) = intern' space xname
  34.159        in name = name' andalso (not require_unique orelse is_unique) end;
  34.160  
  34.161      fun ext [] = if valid false name then name else Long_Name.hidden name
  34.162 @@ -236,7 +244,7 @@
  34.163    Completion.make (xname, pos) (fn completed =>
  34.164      let
  34.165        fun result_ord ((xname1, (_, name1)), (xname2, (_, name2))) =
  34.166 -        (case bool_ord (apply2 Long_Name.is_local (name2, name1)) of
  34.167 +        (case bool_ord (apply2 (is_some o Long_Name.dest_local) (name2, name1)) of
  34.168            EQUAL =>
  34.169              (case int_ord (apply2 Long_Name.qualification (xname1, xname2)) of
  34.170                EQUAL => string_ord (xname1, xname2)
  34.171 @@ -284,41 +292,54 @@
  34.172  (* datatype naming *)
  34.173  
  34.174  datatype naming = Naming of
  34.175 - {private: bool,
  34.176 + {scopes: Binding.scope list,
  34.177 +  private: Binding.scope option,
  34.178    concealed: bool,
  34.179    group: serial option,
  34.180    theory_name: string,
  34.181    path: (string * bool) list};
  34.182  
  34.183 -fun make_naming (private, concealed, group, theory_name, path) =
  34.184 -  Naming {private = private, concealed = concealed, group = group,
  34.185 -    theory_name = theory_name, path = path};
  34.186 +fun make_naming (scopes, private, concealed, group, theory_name, path) =
  34.187 +  Naming {scopes = scopes, private = private, concealed = concealed,
  34.188 +    group = group, theory_name = theory_name, path = path};
  34.189  
  34.190 -fun map_naming f (Naming {private, concealed, group, theory_name, path}) =
  34.191 -  make_naming (f (private, concealed, group, theory_name, path));
  34.192 +fun map_naming f (Naming {scopes, private, concealed, group, theory_name, path}) =
  34.193 +  make_naming (f (scopes, private, concealed, group, theory_name, path));
  34.194  
  34.195 -fun map_path f = map_naming (fn (private, concealed, group, theory_name, path) =>
  34.196 -  (private, concealed, group, theory_name, f path));
  34.197 +fun map_path f = map_naming (fn (scopes, private, concealed, group, theory_name, path) =>
  34.198 +  (scopes, private, concealed, group, theory_name, f path));
  34.199  
  34.200  
  34.201 -val private = map_naming (fn (_, concealed, group, theory_name, path) =>
  34.202 -  (true, concealed, group, theory_name, path));
  34.203 +fun get_scopes (Naming {scopes, ...}) = scopes;
  34.204 +val get_scope = try hd o get_scopes;
  34.205  
  34.206 -val concealed = map_naming (fn (private, _, group, theory_name, path) =>
  34.207 -  (private, true, group, theory_name, path));
  34.208 +fun new_scope naming =
  34.209 +  let
  34.210 +    val scope = Binding.new_scope ();
  34.211 +    val naming' =
  34.212 +      naming |> map_naming (fn (scopes, private, concealed, group, theory_name, path) =>
  34.213 +        (scope :: scopes, private, concealed, group, theory_name, path));
  34.214 +  in (scope, naming') end;
  34.215  
  34.216 -fun set_theory_name theory_name = map_naming (fn (private, concealed, group, _, path) =>
  34.217 -  (private, concealed, group, theory_name, path));
  34.218 +fun private scope = map_naming (fn (scopes, _, concealed, group, theory_name, path) =>
  34.219 +  (scopes, SOME scope, concealed, group, theory_name, path));
  34.220  
  34.221 +val concealed = map_naming (fn (scopes, private, _, group, theory_name, path) =>
  34.222 +  (scopes, private, true, group, theory_name, path));
  34.223 +
  34.224 +fun set_theory_name theory_name = map_naming (fn (scopes, private, concealed, group, _, path) =>
  34.225 +  (scopes, private, concealed, group, theory_name, path));
  34.226  
  34.227  fun get_group (Naming {group, ...}) = group;
  34.228  
  34.229 -fun set_group group = map_naming (fn (private, concealed, _, theory_name, path) =>
  34.230 -  (private, concealed, group, theory_name, path));
  34.231 +fun set_group group = map_naming (fn (scopes, private, concealed, _, theory_name, path) =>
  34.232 +  (scopes, private, concealed, group, theory_name, path));
  34.233  
  34.234  fun new_group naming = set_group (SOME (serial ())) naming;
  34.235  val reset_group = set_group NONE;
  34.236  
  34.237 +fun get_path (Naming {path, ...}) = path;
  34.238 +
  34.239  fun add_path elems = map_path (fn path => path @ [(elems, false)]);
  34.240  val root_path = map_path (fn _ => []);
  34.241  val parent_path = map_path (perhaps (try (#1 o split_last)));
  34.242 @@ -327,33 +348,25 @@
  34.243  fun qualified_path mandatory binding = map_path (fn path =>
  34.244    path @ Binding.path_of (Binding.qualified mandatory "" binding));
  34.245  
  34.246 -val global_naming = make_naming (false, false, NONE, "", []);
  34.247 +val global_naming = make_naming ([], NONE, false, NONE, "", []);
  34.248  val local_naming = global_naming |> add_path Long_Name.localN;
  34.249  
  34.250  
  34.251 +(* visibility flags *)
  34.252 +
  34.253 +fun transform_naming (Naming {private = private', concealed = concealed', ...}) =
  34.254 +  fold private (the_list private') #>
  34.255 +  concealed' ? concealed;
  34.256 +
  34.257 +fun transform_binding (Naming {private, concealed, ...}) =
  34.258 +  Binding.private_default private #>
  34.259 +  concealed ? Binding.concealed;
  34.260 +
  34.261 +
  34.262  (* full name *)
  34.263  
  34.264 -fun err_bad binding = error (Binding.bad binding);
  34.265 -
  34.266 -fun transform_binding (Naming {private, concealed, ...}) =
  34.267 -  private ? Binding.private #>
  34.268 -  concealed ? Binding.concealed;
  34.269 -
  34.270 -val bad_specs = ["", "??", "__"];
  34.271 -
  34.272 -fun name_spec (naming as Naming {path = path1, ...}) raw_binding =
  34.273 -  let
  34.274 -    val binding = transform_binding naming raw_binding;
  34.275 -    val {private, concealed, path = path2, name} = Binding.dest binding;
  34.276 -    val _ = Long_Name.is_qualified name andalso err_bad binding;
  34.277 -
  34.278 -    val spec1 = maps (fn (a, b) => map (rpair b) (Long_Name.explode a)) (path1 @ path2);
  34.279 -    val spec2 = if name = "" then [] else [(name, true)];
  34.280 -    val spec = spec1 @ spec2;
  34.281 -    val _ =
  34.282 -      exists (fn (a, _) => member (op =) bad_specs a orelse exists_string (fn s => s = "\"") a) spec
  34.283 -      andalso err_bad binding;
  34.284 -  in {private = private, concealed = concealed, spec = if null spec2 then [] else spec} end;
  34.285 +fun name_spec naming binding =
  34.286 +  Binding.name_spec (get_scopes naming) (get_path naming) (transform_binding naming binding);
  34.287  
  34.288  fun full_name naming =
  34.289    name_spec naming #> #spec #> map #1 #> Long_Name.implode;
  34.290 @@ -374,7 +387,7 @@
  34.291  
  34.292  fun accesses naming binding =
  34.293    (case name_spec naming binding of
  34.294 -    {private = true, ...} => ([], [])
  34.295 +    {accessible = false, ...} => ([], [])
  34.296    | {spec, ...} =>
  34.297        let
  34.298          val sfxs = mandatory_suffixes spec;
  34.299 @@ -387,10 +400,10 @@
  34.300  fun hide fully name space =
  34.301    space |> map_name_space (fn (kind, internals, entries) =>
  34.302      let
  34.303 -      val _ = Change_Table.defined entries name orelse error (undefined kind name);
  34.304 +      val _ = the_entry space name;
  34.305        val names = valid_accesses space name;
  34.306        val internals' = internals
  34.307 -        |> add_name' name name
  34.308 +        |> hide_name name
  34.309          |> fold (del_name name)
  34.310            (if fully then names else inter (op =) [Long_Name.base_name name] names)
  34.311          |> fold (del_name_extra name) (get_accesses space name);
  34.312 @@ -402,7 +415,7 @@
  34.313  fun alias naming binding name space =
  34.314    space |> map_name_space (fn (kind, internals, entries) =>
  34.315      let
  34.316 -      val _ = Change_Table.defined entries name orelse error (undefined kind name);
  34.317 +      val _ = the_entry space name;
  34.318        val (accs, accs') = accesses naming binding;
  34.319        val internals' = internals |> fold (add_name name) accs;
  34.320        val entries' = entries
  34.321 @@ -446,7 +459,7 @@
  34.322      val (accs, accs') = accesses naming binding;
  34.323  
  34.324      val name = Long_Name.implode (map fst spec);
  34.325 -    val _ = name = "" andalso err_bad binding;
  34.326 +    val _ = name = "" andalso error (Binding.bad binding);
  34.327  
  34.328      val (proper_pos, pos) = Position.default (Binding.pos_of binding);
  34.329      val entry =
  34.330 @@ -498,7 +511,7 @@
  34.331          let
  34.332            val completions = map (fn pos => completion context space (xname, pos)) ps;
  34.333          in
  34.334 -          error (undefined (kind_of space) name ^ Position.here_list ps ^
  34.335 +          error (undefined space name ^ Position.here_list ps ^
  34.336              Markup.markup_report (implode (map Completion.reported_text completions)))
  34.337          end)
  34.338    end;
  34.339 @@ -509,12 +522,14 @@
  34.340      val _ = Position.reports reports;
  34.341    in (name, x) end;
  34.342  
  34.343 +fun defined (Table (_, tab)) name = Change_Table.defined tab name;
  34.344 +fun lookup (Table (_, tab)) name = Change_Table.lookup tab name;
  34.345  fun lookup_key (Table (_, tab)) name = Change_Table.lookup_key tab name;
  34.346  
  34.347  fun get table name =
  34.348    (case lookup_key table name of
  34.349      SOME (_, x) => x
  34.350 -  | NONE => error (undefined (kind_of (space_of_table table)) name));
  34.351 +  | NONE => error (undefined (space_of_table table) name));
  34.352  
  34.353  fun define context strict (binding, x) (Table (space, tab)) =
  34.354    let
    35.1 --- a/src/Pure/Isar/bundle.ML	Wed Apr 01 19:17:41 2015 +0200
    35.2 +++ b/src/Pure/Isar/bundle.ML	Wed Apr 01 22:40:41 2015 +0200
    35.3 @@ -20,9 +20,10 @@
    35.4    val include_cmd: (xstring * Position.T) list -> Proof.state -> Proof.state
    35.5    val including: string list -> Proof.state -> Proof.state
    35.6    val including_cmd: (xstring * Position.T) list -> Proof.state -> Proof.state
    35.7 -  val context: string list -> Element.context_i list -> generic_theory -> local_theory
    35.8 +  val context: string list -> Element.context_i list ->
    35.9 +    generic_theory -> Binding.scope * local_theory
   35.10    val context_cmd: (xstring * Position.T) list -> Element.context list ->
   35.11 -    generic_theory -> local_theory
   35.12 +    generic_theory -> Binding.scope * local_theory
   35.13    val print_bundles: Proof.context -> unit
   35.14  end;
   35.15  
   35.16 @@ -97,8 +98,8 @@
   35.17        |> gen_includes get raw_incls
   35.18        |> prep_decl ([], []) I raw_elems;
   35.19    in
   35.20 -    lthy' |> Local_Theory.open_target
   35.21 -      (Local_Theory.naming_of lthy) (Local_Theory.operations_of lthy) after_close
   35.22 +    lthy' |> Local_Theory.init_target
   35.23 +      (Local_Theory.background_naming_of lthy) (Local_Theory.operations_of lthy) after_close
   35.24    end;
   35.25  
   35.26  in
   35.27 @@ -137,4 +138,3 @@
   35.28    end |> Pretty.writeln_chunks;
   35.29  
   35.30  end;
   35.31 -
    36.1 --- a/src/Pure/Isar/class.ML	Wed Apr 01 19:17:41 2015 +0200
    36.2 +++ b/src/Pure/Isar/class.ML	Wed Apr 01 22:40:41 2015 +0200
    36.3 @@ -599,8 +599,6 @@
    36.4  
    36.5  fun instantiation (tycos, vs, sort) thy =
    36.6    let
    36.7 -    val naming = Sign.naming_of thy;
    36.8 -
    36.9      val _ = if null tycos then error "At least one arity must be given" else ();
   36.10      val class_params = these_params thy (filter (can (Axclass.get_info thy)) sort);
   36.11      fun get_param tyco (param, (_, (c, ty))) =
   36.12 @@ -637,7 +635,7 @@
   36.13      |> Overloading.activate_improvable_syntax
   36.14      |> Context.proof_map (Syntax_Phases.term_check 0 "resorting" resort_check)
   36.15      |> synchronize_inst_syntax
   36.16 -    |> Local_Theory.init naming
   36.17 +    |> Local_Theory.init (Sign.naming_of thy)
   36.18         {define = Generic_Target.define foundation,
   36.19          notes = Generic_Target.notes Generic_Target.theory_notes,
   36.20          abbrev = Generic_Target.abbrev Generic_Target.theory_abbrev,
    37.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    37.2 +++ b/src/Pure/Isar/experiment.ML	Wed Apr 01 22:40:41 2015 +0200
    37.3 @@ -0,0 +1,29 @@
    37.4 +(*  Title:      Pure/Isar/experiment.ML
    37.5 +    Author:     Makarius
    37.6 +
    37.7 +Target for specification experiments that are mostly private.
    37.8 +*)
    37.9 +
   37.10 +signature EXPERIMENT =
   37.11 +sig
   37.12 +  val experiment: Element.context_i list -> theory -> Binding.scope * local_theory
   37.13 +  val experiment_cmd: Element.context list -> theory -> Binding.scope * local_theory
   37.14 +end;
   37.15 +
   37.16 +structure Experiment: EXPERIMENT =
   37.17 +struct
   37.18 +
   37.19 +fun gen_experiment add_locale elems thy =
   37.20 +  let
   37.21 +    val (_, lthy) = thy
   37.22 +      |> add_locale (Binding.name ("experiment" ^ serial_string ())) Binding.empty ([], []) elems;
   37.23 +    val (scope, naming) =
   37.24 +      Name_Space.new_scope (Proof_Context.naming_of (Local_Theory.target_of lthy));
   37.25 +    val naming' = naming |> Name_Space.private scope;
   37.26 +    val lthy' = lthy |> Local_Theory.map_contexts (K (Proof_Context.map_naming (K naming')));
   37.27 +  in (scope, lthy') end;
   37.28 +
   37.29 +val experiment = gen_experiment Expression.add_locale;
   37.30 +val experiment_cmd = gen_experiment Expression.add_locale_cmd;
   37.31 +
   37.32 +end;
    38.1 --- a/src/Pure/Isar/isar_syn.ML	Wed Apr 01 19:17:41 2015 +0200
    38.2 +++ b/src/Pure/Isar/isar_syn.ML	Wed Apr 01 22:40:41 2015 +0200
    38.3 @@ -361,7 +361,7 @@
    38.4      ((Parse.position Parse.xname >> (fn name =>
    38.5          Toplevel.begin_local_theory true (Named_Target.begin name)) ||
    38.6        Scan.optional Parse_Spec.includes [] -- Scan.repeat Parse_Spec.context_element
    38.7 -        >> (fn (incls, elems) => Toplevel.open_target (Bundle.context_cmd incls elems)))
    38.8 +        >> (fn (incls, elems) => Toplevel.open_target (#2 o Bundle.context_cmd incls elems)))
    38.9        --| Parse.begin);
   38.10  
   38.11  
   38.12 @@ -373,13 +373,19 @@
   38.13    Scan.repeat1 Parse_Spec.context_element >> pair ([], []);
   38.14  
   38.15  val _ =
   38.16 -  Outer_Syntax.command @{command_spec "locale"} "define named proof context"
   38.17 +  Outer_Syntax.command @{command_spec "locale"} "define named specification context"
   38.18      (Parse.binding --
   38.19        Scan.optional (@{keyword "="} |-- Parse.!!! locale_val) (([], []), []) -- Parse.opt_begin
   38.20        >> (fn ((name, (expr, elems)), begin) =>
   38.21            Toplevel.begin_local_theory begin
   38.22              (Expression.add_locale_cmd name Binding.empty expr elems #> snd)));
   38.23  
   38.24 +val _ =
   38.25 +  Outer_Syntax.command @{command_spec "experiment"} "open private specification context"
   38.26 +    (Scan.repeat Parse_Spec.context_element --| Parse.begin
   38.27 +      >> (fn elems =>
   38.28 +          Toplevel.begin_local_theory true (Experiment.experiment_cmd elems #> snd)));
   38.29 +
   38.30  fun interpretation_args mandatory =
   38.31    Parse.!!! (Parse_Spec.locale_expression mandatory) --
   38.32      Scan.optional
    39.1 --- a/src/Pure/Isar/local_theory.ML	Wed Apr 01 19:17:41 2015 +0200
    39.2 +++ b/src/Pure/Isar/local_theory.ML	Wed Apr 01 22:40:41 2015 +0200
    39.3 @@ -21,17 +21,14 @@
    39.4    val assert_bottom: bool -> local_theory -> local_theory
    39.5    val mark_brittle: local_theory -> local_theory
    39.6    val assert_nonbrittle: local_theory -> local_theory
    39.7 -  val open_target: Name_Space.naming -> operations -> (local_theory -> local_theory) ->
    39.8 +  val map_contexts: (int -> Proof.context -> Proof.context) -> local_theory -> local_theory
    39.9 +  val background_naming_of: local_theory -> Name_Space.naming
   39.10 +  val map_background_naming: (Name_Space.naming -> Name_Space.naming) ->
   39.11      local_theory -> local_theory
   39.12 -  val close_target: local_theory -> local_theory
   39.13 -  val map_contexts: (int -> Proof.context -> Proof.context) -> local_theory -> local_theory
   39.14 -  val naming_of: local_theory -> Name_Space.naming
   39.15 +  val restore_background_naming: local_theory -> local_theory -> local_theory
   39.16    val full_name: local_theory -> binding -> string
   39.17 -  val map_naming: (Name_Space.naming -> Name_Space.naming) -> local_theory -> local_theory
   39.18 -  val concealed: local_theory -> local_theory
   39.19    val new_group: local_theory -> local_theory
   39.20    val reset_group: local_theory -> local_theory
   39.21 -  val restore_naming: local_theory -> local_theory -> local_theory
   39.22    val standard_morphism: local_theory -> Proof.context -> morphism
   39.23    val standard_form: local_theory -> Proof.context -> (morphism -> 'a) -> 'a
   39.24    val raw_theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
   39.25 @@ -73,6 +70,10 @@
   39.26    val exit_global: local_theory -> theory
   39.27    val exit_result: (morphism -> 'a -> 'b) -> 'a * local_theory -> 'b * Proof.context
   39.28    val exit_result_global: (morphism -> 'a -> 'b) -> 'a * local_theory -> 'b * theory
   39.29 +  val init_target: Name_Space.naming -> operations -> (local_theory -> local_theory) ->
   39.30 +    local_theory -> Binding.scope * local_theory
   39.31 +  val open_target: local_theory -> Binding.scope * local_theory
   39.32 +  val close_target: local_theory -> local_theory
   39.33  end;
   39.34  
   39.35  structure Local_Theory: LOCAL_THEORY =
   39.36 @@ -97,15 +98,15 @@
   39.37    exit: local_theory -> Proof.context};
   39.38  
   39.39  type lthy =
   39.40 - {naming: Name_Space.naming,
   39.41 + {background_naming: Name_Space.naming,
   39.42    operations: operations,
   39.43    after_close: local_theory -> local_theory,
   39.44    brittle: bool,
   39.45    target: Proof.context};
   39.46  
   39.47 -fun make_lthy (naming, operations, after_close, brittle, target) : lthy =
   39.48 -  {naming = naming, operations = operations, after_close = after_close,
   39.49 -    brittle = brittle, target = target};
   39.50 +fun make_lthy (background_naming, operations, after_close, brittle, target) : lthy =
   39.51 +  {background_naming = background_naming, operations = operations,
   39.52 +    after_close = after_close, brittle = brittle, target = target};
   39.53  
   39.54  
   39.55  (* context data *)
   39.56 @@ -124,8 +125,8 @@
   39.57  
   39.58  fun map_top f =
   39.59    assert #>
   39.60 -  Data.map (fn {naming, operations, after_close, brittle, target} :: parents =>
   39.61 -    make_lthy (f (naming, operations, after_close, brittle, target)) :: parents);
   39.62 +  Data.map (fn {background_naming, operations, after_close, brittle, target} :: parents =>
   39.63 +    make_lthy (f (background_naming, operations, after_close, brittle, target)) :: parents);
   39.64  
   39.65  fun restore lthy = #target (top_of lthy) |> Data.put (Data.get lthy);
   39.66  
   39.67 @@ -144,25 +145,16 @@
   39.68      else lthy
   39.69    end;
   39.70  
   39.71 -fun open_target naming operations after_close target =
   39.72 -  assert target
   39.73 -  |> Data.map (cons (make_lthy (naming, operations, after_close, true, target)));
   39.74 -
   39.75 -fun close_target lthy =
   39.76 -  let
   39.77 -    val _ = assert_bottom false lthy;
   39.78 -    val ({after_close, ...} :: rest) = Data.get lthy;
   39.79 -  in lthy |> Data.put rest |> restore |> after_close end;
   39.80 -
   39.81  fun map_contexts f lthy =
   39.82    let val n = level lthy in
   39.83 -    lthy |> (Data.map o map_index) (fn (i, {naming, operations, after_close, brittle, target}) =>
   39.84 -      make_lthy (naming, operations, after_close, brittle,
   39.85 -        target
   39.86 -        |> Context_Position.set_visible false
   39.87 -        |> f (n - i - 1)
   39.88 -        |> Context_Position.restore_visible target))
   39.89 -    |> f n
   39.90 +    lthy |> (Data.map o map_index)
   39.91 +      (fn (i, {background_naming, operations, after_close, brittle, target}) =>
   39.92 +        make_lthy (background_naming, operations, after_close, brittle,
   39.93 +          target
   39.94 +          |> Context_Position.set_visible false
   39.95 +          |> f (n - i - 1)
   39.96 +          |> Context_Position.restore_visible target))
   39.97 +      |> f n
   39.98    end;
   39.99  
  39.100  
  39.101 @@ -170,8 +162,8 @@
  39.102  
  39.103  fun mark_brittle lthy =
  39.104    if level lthy = 1 then
  39.105 -    map_top (fn (naming, operations, after_close, _, target) =>
  39.106 -      (naming, operations, after_close, true, target)) lthy
  39.107 +    map_top (fn (background_naming, operations, after_close, _, target) =>
  39.108 +      (background_naming, operations, after_close, true, target)) lthy
  39.109    else lthy;
  39.110  
  39.111  fun assert_nonbrittle lthy =
  39.112 @@ -179,20 +171,20 @@
  39.113    else lthy;
  39.114  
  39.115  
  39.116 -(* naming *)
  39.117 +(* naming for background theory *)
  39.118  
  39.119 -val naming_of = #naming o top_of;
  39.120 -val full_name = Name_Space.full_name o naming_of;
  39.121 +val background_naming_of = #background_naming o top_of;
  39.122  
  39.123 -fun map_naming f =
  39.124 -  map_top (fn (naming, operations, after_close, brittle, target) =>
  39.125 -    (f naming, operations, after_close, brittle, target));
  39.126 +fun map_background_naming f =
  39.127 +  map_top (fn (background_naming, operations, after_close, brittle, target) =>
  39.128 +    (f background_naming, operations, after_close, brittle, target));
  39.129  
  39.130 -val concealed = map_naming Name_Space.concealed;
  39.131 -val new_group = map_naming Name_Space.new_group;
  39.132 -val reset_group = map_naming Name_Space.reset_group;
  39.133 +val restore_background_naming = map_background_naming o K o background_naming_of;
  39.134  
  39.135 -val restore_naming = map_naming o K o naming_of;
  39.136 +val full_name = Name_Space.full_name o background_naming_of;
  39.137 +
  39.138 +val new_group = map_background_naming Name_Space.new_group;
  39.139 +val reset_group = map_background_naming Name_Space.reset_group;
  39.140  
  39.141  
  39.142  (* standard morphisms *)
  39.143 @@ -200,7 +192,7 @@
  39.144  fun standard_morphism lthy ctxt =
  39.145    Proof_Context.norm_export_morphism lthy ctxt $>
  39.146    Morphism.binding_morphism "Local_Theory.standard_binding"
  39.147 -    (Name_Space.transform_binding (naming_of lthy));
  39.148 +    (Name_Space.transform_binding (Proof_Context.naming_of lthy));
  39.149  
  39.150  fun standard_form lthy ctxt x =
  39.151    Morphism.form (Morphism.transform (standard_morphism lthy ctxt) x);
  39.152 @@ -217,11 +209,17 @@
  39.153  fun raw_theory f = #2 o raw_theory_result (f #> pair ());
  39.154  
  39.155  fun background_theory_result f lthy =
  39.156 -  lthy |> raw_theory_result (fn thy =>
  39.157 -    thy
  39.158 -    |> Sign.map_naming (K (naming_of lthy))
  39.159 -    |> f
  39.160 -    ||> Sign.restore_naming thy);
  39.161 +  let
  39.162 +    val naming =
  39.163 +      background_naming_of lthy
  39.164 +      |> Name_Space.transform_naming (Proof_Context.naming_of lthy);
  39.165 +  in
  39.166 +    lthy |> raw_theory_result (fn thy =>
  39.167 +      thy
  39.168 +      |> Sign.map_naming (K naming)
  39.169 +      |> f
  39.170 +      ||> Sign.restore_naming thy)
  39.171 +  end;
  39.172  
  39.173  fun background_theory f = #2 o background_theory_result (f #> pair ());
  39.174  
  39.175 @@ -339,18 +337,15 @@
  39.176  
  39.177  
  39.178  
  39.179 -(** init and exit **)
  39.180 +(** manage targets **)
  39.181  
  39.182 -(* init *)
  39.183 +(* outermost target *)
  39.184  
  39.185 -fun init naming operations target =
  39.186 +fun init background_naming operations target =
  39.187    target |> Data.map
  39.188 -    (fn [] => [make_lthy (naming, operations, I, false, target)]
  39.189 +    (fn [] => [make_lthy (background_naming, operations, I, false, target)]
  39.190        | _ => error "Local theory already initialized");
  39.191  
  39.192 -
  39.193 -(* exit *)
  39.194 -
  39.195  val exit = operation #exit;
  39.196  val exit_global = Proof_Context.theory_of o exit;
  39.197  
  39.198 @@ -367,4 +362,25 @@
  39.199      val phi = standard_morphism lthy thy_ctxt;
  39.200    in (f phi x, thy) end;
  39.201  
  39.202 +
  39.203 +(* nested targets *)
  39.204 +
  39.205 +fun init_target background_naming operations after_close lthy =
  39.206 +  let
  39.207 +    val _ = assert lthy;
  39.208 +    val (scope, target) = Proof_Context.new_scope lthy;
  39.209 +    val lthy' =
  39.210 +      target
  39.211 +      |> Data.map (cons (make_lthy (background_naming, operations, after_close, true, target)));
  39.212 +  in (scope, lthy') end;
  39.213 +
  39.214 +fun open_target lthy =
  39.215 +  init_target (background_naming_of lthy) (operations_of lthy) I lthy;
  39.216 +
  39.217 +fun close_target lthy =
  39.218 +  let
  39.219 +    val _ = assert_bottom false lthy;
  39.220 +    val ({after_close, ...} :: rest) = Data.get lthy;
  39.221 +  in lthy |> Data.put rest |> restore |> after_close end;
  39.222 +
  39.223  end;
    40.1 --- a/src/Pure/Isar/locale.ML	Wed Apr 01 19:17:41 2015 +0200
    40.2 +++ b/src/Pure/Isar/locale.ML	Wed Apr 01 22:40:41 2015 +0200
    40.3 @@ -180,7 +180,7 @@
    40.4  fun markup_name ctxt name = markup_extern ctxt name |-> Markup.markup;
    40.5  fun pretty_name ctxt name = markup_extern ctxt name |> Pretty.mark_str;
    40.6  
    40.7 -val get_locale = Option.map #2 oo (Name_Space.lookup_key o Locales.get);
    40.8 +val get_locale = Name_Space.lookup o Locales.get;
    40.9  val defined = is_some oo get_locale;
   40.10  
   40.11  fun the_locale thy name =
    41.1 --- a/src/Pure/Isar/named_target.ML	Wed Apr 01 19:17:41 2015 +0200
    41.2 +++ b/src/Pure/Isar/named_target.ML	Wed Apr 01 22:40:41 2015 +0200
    41.3 @@ -155,14 +155,14 @@
    41.4  fun gen_init before_exit target thy =
    41.5    let
    41.6      val name_data = make_name_data thy target;
    41.7 -    val naming = Sign.naming_of thy
    41.8 -      |> Name_Space.mandatory_path (Long_Name.base_name target);
    41.9 +    val background_naming =
   41.10 +      Sign.naming_of thy |> Name_Space.mandatory_path (Long_Name.base_name target);
   41.11    in
   41.12      thy
   41.13      |> Sign.change_begin
   41.14      |> init_context name_data
   41.15      |> is_none before_exit ? Data.put (SOME name_data)
   41.16 -    |> Local_Theory.init naming
   41.17 +    |> Local_Theory.init background_naming
   41.18         {define = Generic_Target.define (foundation name_data),
   41.19          notes = Generic_Target.notes (notes name_data),
   41.20          abbrev = Generic_Target.abbrev (abbrev name_data),
    42.1 --- a/src/Pure/Isar/overloading.ML	Wed Apr 01 19:17:41 2015 +0200
    42.2 +++ b/src/Pure/Isar/overloading.ML	Wed Apr 01 22:40:41 2015 +0200
    42.3 @@ -189,7 +189,6 @@
    42.4  fun gen_overloading prep_const raw_overloading thy =
    42.5    let
    42.6      val ctxt = Proof_Context.init_global thy;
    42.7 -    val naming = Sign.naming_of thy;
    42.8      val _ = if null raw_overloading then error "At least one parameter must be given" else ();
    42.9      val overloading = raw_overloading |> map (fn (v, const, checked) =>
   42.10        (Term.dest_Const (prep_const ctxt const), (v, checked)));
   42.11 @@ -201,7 +200,7 @@
   42.12      |> fold (fn ((_, ty), (v, _)) => Variable.declare_names (Free (v, ty))) overloading
   42.13      |> activate_improvable_syntax
   42.14      |> synchronize_syntax
   42.15 -    |> Local_Theory.init naming
   42.16 +    |> Local_Theory.init (Sign.naming_of thy)
   42.17         {define = Generic_Target.define foundation,
   42.18          notes = Generic_Target.notes Generic_Target.theory_notes,
   42.19          abbrev = Generic_Target.abbrev Generic_Target.theory_abbrev,
    43.1 --- a/src/Pure/Isar/proof_context.ML	Wed Apr 01 19:17:41 2015 +0200
    43.2 +++ b/src/Pure/Isar/proof_context.ML	Wed Apr 01 22:40:41 2015 +0200
    43.3 @@ -34,6 +34,10 @@
    43.4    val naming_of: Proof.context -> Name_Space.naming
    43.5    val restore_naming: Proof.context -> Proof.context -> Proof.context
    43.6    val full_name: Proof.context -> binding -> string
    43.7 +  val get_scope: Proof.context -> Binding.scope option
    43.8 +  val new_scope: Proof.context -> Binding.scope * Proof.context
    43.9 +  val private: Binding.scope -> Proof.context -> Proof.context
   43.10 +  val concealed: Proof.context -> Proof.context
   43.11    val class_space: Proof.context -> Name_Space.T
   43.12    val type_space: Proof.context -> Name_Space.T
   43.13    val const_space: Proof.context -> Name_Space.T
   43.14 @@ -304,6 +308,17 @@
   43.15  
   43.16  val full_name = Name_Space.full_name o naming_of;
   43.17  
   43.18 +val get_scope = Name_Space.get_scope o naming_of;
   43.19 +
   43.20 +fun new_scope ctxt =
   43.21 +  let
   43.22 +    val (scope, naming') = Name_Space.new_scope (naming_of ctxt);
   43.23 +    val ctxt' = map_naming (K naming') ctxt;
   43.24 +  in (scope, ctxt') end;
   43.25 +
   43.26 +val private = map_naming o Name_Space.private;
   43.27 +val concealed = map_naming Name_Space.concealed;
   43.28 +
   43.29  
   43.30  (* name spaces *)
   43.31  
    44.1 --- a/src/Pure/ML/ml_antiquotations.ML	Wed Apr 01 19:17:41 2015 +0200
    44.2 +++ b/src/Pure/ML/ml_antiquotations.ML	Wed Apr 01 22:40:41 2015 +0200
    44.3 @@ -47,7 +47,7 @@
    44.4                      |> filter completed
    44.5                      |> map (fn a => (a, ("system_option", a))));
    44.6                val report = Markup.markup_report (Completion.reported_text completion);
    44.7 -            in cat_error msg report end;
    44.8 +            in error (msg ^ report) end;
    44.9          val _ = Context_Position.report ctxt pos markup;
   44.10        in ML_Syntax.print_string name end)) #>
   44.11  
    45.1 --- a/src/Pure/PIDE/batch_session.scala	Wed Apr 01 19:17:41 2015 +0200
    45.2 +++ b/src/Pure/PIDE/batch_session.scala	Wed Apr 01 22:40:41 2015 +0200
    45.3 @@ -19,7 +19,7 @@
    45.4      session: String): Batch_Session =
    45.5    {
    45.6      val (_, session_tree) =
    45.7 -      Build.find_sessions(options, dirs).selection(false, false, Nil, List(session))
    45.8 +      Build.find_sessions(options, dirs).selection(sessions = List(session))
    45.9      val session_info = session_tree(session)
   45.10      val parent_session =
   45.11        session_info.parent getOrElse error("No parent session for " + quote(session))
   45.12 @@ -29,7 +29,7 @@
   45.13          dirs = dirs, sessions = List(parent_session)) != 0)
   45.14        new RuntimeException
   45.15  
   45.16 -    val deps = Build.dependencies(Build.Ignore_Progress, false, verbose, false, session_tree)
   45.17 +    val deps = Build.dependencies(verbose = verbose, tree = session_tree)
   45.18      val resources =
   45.19      {
   45.20        val content = deps(parent_session)
    46.1 --- a/src/Pure/Pure.thy	Wed Apr 01 19:17:41 2015 +0200
    46.2 +++ b/src/Pure/Pure.thy	Wed Apr 01 22:40:41 2015 +0200
    46.3 @@ -33,7 +33,7 @@
    46.4    and "bundle" :: thy_decl
    46.5    and "include" "including" :: prf_decl
    46.6    and "print_bundles" :: diag
    46.7 -  and "context" "locale" :: thy_decl_block
    46.8 +  and "context" "locale" "experiment" :: thy_decl_block
    46.9    and "sublocale" "interpretation" :: thy_goal
   46.10    and "interpret" :: prf_goal % "proof"
   46.11    and "class" :: thy_decl_block
    47.1 --- a/src/Pure/ROOT	Wed Apr 01 19:17:41 2015 +0200
    47.2 +++ b/src/Pure/ROOT	Wed Apr 01 22:40:41 2015 +0200
    47.3 @@ -121,6 +121,7 @@
    47.4      "Isar/code.ML"
    47.5      "Isar/context_rules.ML"
    47.6      "Isar/element.ML"
    47.7 +    "Isar/experiment.ML"
    47.8      "Isar/expression.ML"
    47.9      "Isar/generic_target.ML"
   47.10      "Isar/isar_cmd.ML"
    48.1 --- a/src/Pure/ROOT.ML	Wed Apr 01 19:17:41 2015 +0200
    48.2 +++ b/src/Pure/ROOT.ML	Wed Apr 01 22:40:41 2015 +0200
    48.3 @@ -273,6 +273,7 @@
    48.4  use "Isar/expression.ML";
    48.5  use "Isar/class_declaration.ML";
    48.6  use "Isar/bundle.ML";
    48.7 +use "Isar/experiment.ML";
    48.8  
    48.9  use "simplifier.ML";
   48.10  use "Tools/plugin.ML";
    49.1 --- a/src/Pure/Tools/build.scala	Wed Apr 01 19:17:41 2015 +0200
    49.2 +++ b/src/Pure/Tools/build.scala	Wed Apr 01 22:40:41 2015 +0200
    49.3 @@ -162,12 +162,18 @@
    49.4      def apply(name: String): Session_Info = graph.get_node(name)
    49.5      def isDefinedAt(name: String): Boolean = graph.defined(name)
    49.6  
    49.7 -    def selection(requirements: Boolean, all_sessions: Boolean,
    49.8 -      session_groups: List[String], sessions: List[String]): (List[String], Session_Tree) =
    49.9 +    def selection(
   49.10 +      requirements: Boolean = false,
   49.11 +      all_sessions: Boolean = false,
   49.12 +      session_groups: List[String] = Nil,
   49.13 +      exclude_sessions: List[String] = Nil,
   49.14 +      sessions: List[String] = Nil): (List[String], Session_Tree) =
   49.15      {
   49.16 -      val bad_sessions = sessions.filterNot(isDefinedAt(_))
   49.17 +      val bad_sessions =
   49.18 +        SortedSet((exclude_sessions ::: sessions).filterNot(isDefinedAt(_)): _*).toList
   49.19        if (bad_sessions.nonEmpty) error("Undefined session(s): " + commas_quote(bad_sessions))
   49.20  
   49.21 +      val excluded = graph.all_succs(exclude_sessions).toSet
   49.22        val pre_selected =
   49.23        {
   49.24          if (all_sessions) graph.keys
   49.25 @@ -179,7 +185,8 @@
   49.26              if info.select || select(name) || apply(name).groups.exists(select_group)
   49.27            } yield name).toList
   49.28          }
   49.29 -      }
   49.30 +      }.filterNot(excluded)
   49.31 +
   49.32        val selected =
   49.33          if (requirements) (graph.all_preds(pre_selected).toSet -- pre_selected).toList
   49.34          else pre_selected
   49.35 @@ -427,8 +434,13 @@
   49.36      def sources(name: String): List[SHA1.Digest] = deps(name).sources.map(_._2)
   49.37    }
   49.38  
   49.39 -  def dependencies(progress: Progress, inlined_files: Boolean,
   49.40 -      verbose: Boolean, list_files: Boolean, tree: Session_Tree): Deps =
   49.41 +  def dependencies(
   49.42 +      progress: Progress = Ignore_Progress,
   49.43 +      inlined_files: Boolean = false,
   49.44 +      verbose: Boolean = false,
   49.45 +      list_files: Boolean = false,
   49.46 +      check_keywords: Set[String] = Set.empty,
   49.47 +      tree: Session_Tree): Deps =
   49.48      Deps((Map.empty[String, Session_Content] /: tree.topological_order)(
   49.49        { case (deps, (name, info)) =>
   49.50            if (progress.stopped) throw Exn.Interrupt()
   49.51 @@ -484,16 +496,20 @@
   49.52              val keywords = thy_deps.keywords
   49.53              val syntax = thy_deps.syntax.asInstanceOf[Outer_Syntax]
   49.54  
   49.55 +            val theory_files = thy_deps.deps.map(dep => Path.explode(dep.name.node))
   49.56              val loaded_files = if (inlined_files) thy_deps.loaded_files else Nil
   49.57  
   49.58              val all_files =
   49.59 -              (thy_deps.deps.map(dep => Path.explode(dep.name.node)) ::: loaded_files :::
   49.60 +              (theory_files ::: loaded_files :::
   49.61                  info.files.map(file => info.dir + file) :::
   49.62                  info.document_files.map(file => info.dir + file._1 + file._2)).map(_.expand)
   49.63  
   49.64              if (list_files)
   49.65                progress.echo(cat_lines(all_files.map(_.implode).sorted.map("  " + _)))
   49.66  
   49.67 +            if (check_keywords.nonEmpty)
   49.68 +              Check_Keywords.check_keywords(progress, syntax.keywords, check_keywords, theory_files)
   49.69 +
   49.70              val sources = all_files.map(p => (p, SHA1.digest(p.file)))
   49.71  
   49.72              val session_graph = thy_deps.deps_graph(info.parent getOrElse "", loaded_theories0)
   49.73 @@ -516,8 +532,8 @@
   49.74      dirs: List[Path],
   49.75      sessions: List[String]): Deps =
   49.76    {
   49.77 -    val (_, tree) = find_sessions(options, dirs = dirs).selection(false, false, Nil, sessions)
   49.78 -    dependencies(Ignore_Progress, inlined_files, false, false, tree)
   49.79 +    val (_, tree) = find_sessions(options, dirs = dirs).selection(sessions = sessions)
   49.80 +    dependencies(inlined_files = inlined_files, tree = tree)
   49.81    }
   49.82  
   49.83    def session_content(
   49.84 @@ -737,18 +753,20 @@
   49.85      session_groups: List[String] = Nil,
   49.86      max_jobs: Int = 1,
   49.87      list_files: Boolean = false,
   49.88 +    check_keywords: Set[String] = Set.empty,
   49.89      no_build: Boolean = false,
   49.90      system_mode: Boolean = false,
   49.91      verbose: Boolean = false,
   49.92 +    exclude_sessions: List[String] = Nil,
   49.93      sessions: List[String] = Nil): Map[String, Int] =
   49.94    {
   49.95      /* session tree and dependencies */
   49.96  
   49.97      val full_tree = find_sessions(options.int("completion_limit") = 0, dirs, select_dirs)
   49.98      val (selected, selected_tree) =
   49.99 -      full_tree.selection(requirements, all_sessions, session_groups, sessions)
  49.100 +      full_tree.selection(requirements, all_sessions, session_groups, exclude_sessions, sessions)
  49.101  
  49.102 -    val deps = dependencies(progress, true, verbose, list_files, selected_tree)
  49.103 +    val deps = dependencies(progress, true, verbose, list_files, check_keywords, selected_tree)
  49.104  
  49.105      def make_stamp(name: String): String =
  49.106        sources_stamp(selected_tree(name).entry_digest :: deps.sources(name))
  49.107 @@ -988,15 +1006,17 @@
  49.108      session_groups: List[String] = Nil,
  49.109      max_jobs: Int = 1,
  49.110      list_files: Boolean = false,
  49.111 +    check_keywords: Set[String] = Set.empty,
  49.112      no_build: Boolean = false,
  49.113      system_mode: Boolean = false,
  49.114      verbose: Boolean = false,
  49.115 +    exclude_sessions: List[String] = Nil,
  49.116      sessions: List[String] = Nil): Int =
  49.117    {
  49.118      val results =
  49.119 -      build_results(options, progress, requirements, all_sessions,
  49.120 -        build_heap, clean_build, dirs, select_dirs, session_groups, max_jobs,
  49.121 -        list_files, no_build, system_mode, verbose, sessions)
  49.122 +      build_results(options, progress, requirements, all_sessions, build_heap, clean_build,
  49.123 +        dirs, select_dirs, session_groups, max_jobs, list_files, check_keywords,
  49.124 +        no_build, system_mode, verbose, exclude_sessions, sessions)
  49.125  
  49.126      val rc = (0 /: results)({ case (rc1, (_, rc2)) => rc1 max rc2 })
  49.127      if (rc != 0 && (verbose || !no_build)) {
  49.128 @@ -1024,13 +1044,15 @@
  49.129            Properties.Value.Boolean(no_build) ::
  49.130            Properties.Value.Boolean(system_mode) ::
  49.131            Properties.Value.Boolean(verbose) ::
  49.132 -          Command_Line.Chunks(dirs, select_dirs, session_groups, build_options, sessions) =>
  49.133 +          Command_Line.Chunks(dirs, select_dirs, session_groups, check_keywords,
  49.134 +              build_options, exclude_sessions, sessions) =>
  49.135              val options = (Options.init() /: build_options)(_ + _)
  49.136              val progress = new Console_Progress(verbose)
  49.137              progress.interrupt_handler {
  49.138                build(options, progress, requirements, all_sessions, build_heap, clean_build,
  49.139                  dirs.map(Path.explode(_)), select_dirs.map(Path.explode(_)), session_groups,
  49.140 -                max_jobs, list_files, no_build, system_mode, verbose, sessions)
  49.141 +                max_jobs, list_files, check_keywords.toSet, no_build, system_mode,
  49.142 +                verbose, exclude_sessions, sessions)
  49.143              }
  49.144          case _ => error("Bad arguments:\n" + cat_lines(args))
  49.145        }
    50.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    50.2 +++ b/src/Pure/Tools/check_keywords.scala	Wed Apr 01 22:40:41 2015 +0200
    50.3 @@ -0,0 +1,54 @@
    50.4 +/*  Title:      Pure/Tools/check_keywords.scala
    50.5 +    Author:     Makarius
    50.6 +
    50.7 +Check theory sources for conflicts with proposed keywords.
    50.8 +*/
    50.9 +
   50.10 +package isabelle
   50.11 +
   50.12 +
   50.13 +object Check_Keywords
   50.14 +{
   50.15 +  def conflicts(
   50.16 +    keywords: Keyword.Keywords,
   50.17 +    check: Set[String],
   50.18 +    input: CharSequence,
   50.19 +    start: Token.Pos): List[(Token, Position.T)] =
   50.20 +  {
   50.21 +    object Parser extends Parse.Parser
   50.22 +    {
   50.23 +      private val conflict =
   50.24 +        position(token("token", tok => !(tok.is_command || tok.is_keyword) && check(tok.source)))
   50.25 +      private val other = token("token", _ => true)
   50.26 +      private val item = conflict ^^ (x => Some(x)) | other ^^ (_ => None)
   50.27 +
   50.28 +      val result =
   50.29 +        parse_all(rep(item), Token.reader(Token.explode(keywords, input), start)) match {
   50.30 +          case Success(res, _) => for (Some(x) <- res) yield x
   50.31 +          case bad => error(bad.toString)
   50.32 +        }
   50.33 +    }
   50.34 +    Parser.result
   50.35 +  }
   50.36 +
   50.37 +  def check_keywords(
   50.38 +    progress: Build.Progress,
   50.39 +    keywords: Keyword.Keywords,
   50.40 +    check: Set[String],
   50.41 +    paths: List[Path])
   50.42 +  {
   50.43 +    val parallel_args = paths.map(path => (File.read(path), Token.Pos.file(path.expand.implode)))
   50.44 +
   50.45 +    val bad =
   50.46 +      Par_List.map((arg: (String, Token.Pos)) => {
   50.47 +        if (progress.stopped) throw Exn.Interrupt()
   50.48 +        conflicts(keywords, check, arg._1, arg._2)
   50.49 +      }, parallel_args).flatten
   50.50 +
   50.51 +    for ((tok, pos) <- bad) {
   50.52 +      progress.echo(Output.warning_text(
   50.53 +        "keyword conflict: " + tok.kind.toString + " " + quote(tok.content) +
   50.54 +          Position.here(pos)))
   50.55 +    }
   50.56 +  }
   50.57 +}
    51.1 --- a/src/Pure/Tools/find_theorems.ML	Wed Apr 01 19:17:41 2015 +0200
    51.2 +++ b/src/Pure/Tools/find_theorems.ML	Wed Apr 01 22:40:41 2015 +0200
    51.3 @@ -328,7 +328,7 @@
    51.4  local
    51.5  
    51.6  val index_ord = option_ord (K EQUAL);
    51.7 -val hidden_ord = bool_ord o apply2 Long_Name.is_hidden;
    51.8 +val hidden_ord = bool_ord o apply2 (is_some o Long_Name.dest_hidden);
    51.9  val qual_ord = int_ord o apply2 Long_Name.qualification;
   51.10  val txt_ord = int_ord o apply2 size;
   51.11  
    52.1 --- a/src/Pure/Tools/named_theorems.ML	Wed Apr 01 19:17:41 2015 +0200
    52.2 +++ b/src/Pure/Tools/named_theorems.ML	Wed Apr 01 22:40:41 2015 +0200
    52.3 @@ -61,7 +61,7 @@
    52.4  
    52.5  fun declare binding descr lthy =
    52.6    let
    52.7 -    val name = Name_Space.full_name (Local_Theory.naming_of lthy) binding;
    52.8 +    val name = Local_Theory.full_name lthy binding;
    52.9      val description =
   52.10        "declaration of " ^ (if descr = "" then Binding.name_of binding ^ " rules" else descr);
   52.11      val lthy' = lthy
   52.12 @@ -86,7 +86,7 @@
   52.13        let
   52.14          val thy = Proof_Context.theory_of ctxt;
   52.15          val name = Global_Theory.check_fact thy (xname, pos);
   52.16 -        val _ = get ctxt name handle ERROR msg => cat_error msg (Position.here pos);
   52.17 +        val _ = get ctxt name handle ERROR msg => error (msg ^ Position.here pos);
   52.18        in ML_Syntax.print_string name end)));
   52.19  
   52.20  end;
    53.1 --- a/src/Pure/Tools/plugin.ML	Wed Apr 01 19:17:41 2015 +0200
    53.2 +++ b/src/Pure/Tools/plugin.ML	Wed Apr 01 22:40:41 2015 +0200
    53.3 @@ -138,9 +138,9 @@
    53.4  
    53.5  fun apply change_naming (interp: interp) (data: data) lthy =
    53.6    lthy
    53.7 -  |> change_naming ? Local_Theory.map_naming (K (#naming data))
    53.8 +  |> change_naming ? Local_Theory.map_background_naming (K (#naming data))
    53.9    |> #apply interp (#value data)
   53.10 -  |> Local_Theory.restore_naming lthy;
   53.11 +  |> Local_Theory.restore_background_naming lthy;
   53.12  
   53.13  fun unfinished data (interp: interp, data') =
   53.14    (interp,
    54.1 --- a/src/Pure/build-jars	Wed Apr 01 19:17:41 2015 +0200
    54.2 +++ b/src/Pure/build-jars	Wed Apr 01 22:40:41 2015 +0200
    54.3 @@ -92,6 +92,7 @@
    54.4    Tools/build.scala
    54.5    Tools/build_console.scala
    54.6    Tools/build_doc.scala
    54.7 +  Tools/check_keywords.scala
    54.8    Tools/check_source.scala
    54.9    Tools/doc.scala
   54.10    Tools/main.scala
    55.1 --- a/src/Pure/facts.ML	Wed Apr 01 19:17:41 2015 +0200
    55.2 +++ b/src/Pure/facts.ML	Wed Apr 01 22:40:41 2015 +0200
    55.3 @@ -166,13 +166,13 @@
    55.4  
    55.5  (* retrieve *)
    55.6  
    55.7 -val defined = is_some oo (Name_Space.lookup_key o facts_of);
    55.8 +val defined = Name_Space.defined o facts_of;
    55.9  
   55.10  fun lookup context facts name =
   55.11 -  (case Name_Space.lookup_key (facts_of facts) name of
   55.12 +  (case Name_Space.lookup (facts_of facts) name of
   55.13      NONE => NONE
   55.14 -  | SOME (_, Static ths) => SOME (true, ths)
   55.15 -  | SOME (_, Dynamic f) => SOME (false, f context));
   55.16 +  | SOME (Static ths) => SOME (true, ths)
   55.17 +  | SOME (Dynamic f) => SOME (false, f context));
   55.18  
   55.19  fun retrieve context facts (xname, pos) =
   55.20    let
    56.1 --- a/src/Pure/sign.ML	Wed Apr 01 19:17:41 2015 +0200
    56.2 +++ b/src/Pure/sign.ML	Wed Apr 01 22:40:41 2015 +0200
    56.3 @@ -101,6 +101,8 @@
    56.4      (string * (Proof.context -> Ast.ast list -> Ast.ast)) list -> theory -> theory
    56.5    val add_trrules: Ast.ast Syntax.trrule list -> theory -> theory
    56.6    val del_trrules: Ast.ast Syntax.trrule list -> theory -> theory
    56.7 +  val get_scope: theory -> Binding.scope option
    56.8 +  val new_scope: theory -> Binding.scope * theory
    56.9    val new_group: theory -> theory
   56.10    val reset_group: theory -> theory
   56.11    val add_path: string -> theory -> theory
   56.12 @@ -109,6 +111,8 @@
   56.13    val mandatory_path: string -> theory -> theory
   56.14    val qualified_path: bool -> binding -> theory -> theory
   56.15    val local_path: theory -> theory
   56.16 +  val private: Binding.scope -> theory -> theory
   56.17 +  val concealed: theory -> theory
   56.18    val hide_class: bool -> string -> theory -> theory
   56.19    val hide_type: bool -> string -> theory -> theory
   56.20    val hide_const: bool -> string -> theory -> theory
   56.21 @@ -499,6 +503,14 @@
   56.22  
   56.23  (* naming *)
   56.24  
   56.25 +val get_scope = Name_Space.get_scope o naming_of;
   56.26 +
   56.27 +fun new_scope thy =
   56.28 +  let
   56.29 +    val (scope, naming') = Name_Space.new_scope (naming_of thy);
   56.30 +    val thy' = map_naming (K naming') thy;
   56.31 +  in (scope, thy') end;
   56.32 +
   56.33  val new_group = map_naming Name_Space.new_group;
   56.34  val reset_group = map_naming Name_Space.reset_group;
   56.35  
   56.36 @@ -510,6 +522,9 @@
   56.37  
   56.38  fun local_path thy = thy |> root_path |> add_path (Context.theory_name thy);
   56.39  
   56.40 +val private = map_naming o Name_Space.private;
   56.41 +val concealed = map_naming Name_Space.concealed;
   56.42 +
   56.43  
   56.44  (* hide names *)
   56.45  
    57.1 --- a/src/Pure/thm.ML	Wed Apr 01 19:17:41 2015 +0200
    57.2 +++ b/src/Pure/thm.ML	Wed Apr 01 22:40:41 2015 +0200
    57.3 @@ -590,8 +590,8 @@
    57.4  fun axiom theory name =
    57.5    let
    57.6      fun get_ax thy =
    57.7 -      Name_Space.lookup_key (Theory.axiom_table thy) name
    57.8 -      |> Option.map (fn (_, prop) =>
    57.9 +      Name_Space.lookup (Theory.axiom_table thy) name
   57.10 +      |> Option.map (fn prop =>
   57.11             let
   57.12               val der = deriv_rule0 (Proofterm.axm_proof name prop);
   57.13               val maxidx = maxidx_of_term prop;
    58.1 --- a/src/Pure/type.ML	Wed Apr 01 19:17:41 2015 +0200
    58.2 +++ b/src/Pure/type.ML	Wed Apr 01 22:40:41 2015 +0200
    58.3 @@ -254,7 +254,7 @@
    58.4  
    58.5  fun undecl_type c = "Undeclared type constructor: " ^ quote c;
    58.6  
    58.7 -fun lookup_type (TSig {types, ...}) = Option.map #2 o Name_Space.lookup_key types;
    58.8 +fun lookup_type (TSig {types, ...}) = Name_Space.lookup types;
    58.9  
   58.10  fun check_decl context (TSig {types, ...}) (c, pos) =
   58.11    Name_Space.check_reports context types (c, [pos]);
   58.12 @@ -659,8 +659,9 @@
   58.13    let
   58.14      val types' = f types;
   58.15      val _ =
   58.16 +      not (Name_Space.defined types' "dummy") orelse
   58.17        Name_Space.intern (Name_Space.space_of_table types') "dummy" = "dummy" orelse
   58.18 -        error "Illegal declaration of dummy type";
   58.19 +      error "Illegal declaration of dummy type";
   58.20    in (classes, default, types') end);
   58.21  
   58.22  fun syntactic tsig (Type (c, Ts)) =
    59.1 --- a/src/Pure/variable.ML	Wed Apr 01 19:17:41 2015 +0200
    59.2 +++ b/src/Pure/variable.ML	Wed Apr 01 22:40:41 2015 +0200
    59.3 @@ -340,14 +340,14 @@
    59.4  fun restore_proper_fixes ctxt = Config.put proper_fixes (Config.get ctxt proper_fixes);
    59.5  
    59.6  fun is_improper ctxt x =
    59.7 -  (case Name_Space.lookup_key (fixes_of ctxt) x of
    59.8 -    SOME (_, (_, proper)) => not proper
    59.9 +  (case Name_Space.lookup (fixes_of ctxt) x of
   59.10 +    SOME (_, proper) => not proper
   59.11    | NONE => false);
   59.12  
   59.13  
   59.14  (* specialized name space *)
   59.15  
   59.16 -val is_fixed = Name_Space.defined_entry o fixes_space;
   59.17 +val is_fixed = Name_Space.defined o fixes_of;
   59.18  fun is_newly_fixed inner outer = is_fixed inner andf (not o is_fixed outer);
   59.19  
   59.20  val fixed_ord = Name_Space.entry_ord o fixes_space;
   59.21 @@ -358,8 +358,8 @@
   59.22    in if is_fixed ctxt x' then SOME x' else NONE end;
   59.23  
   59.24  fun revert_fixed ctxt x =
   59.25 -  (case Name_Space.lookup_key (fixes_of ctxt) x of
   59.26 -    SOME (_, (x', _)) => if intern_fixed ctxt x' = x then x' else x
   59.27 +  (case Name_Space.lookup (fixes_of ctxt) x of
   59.28 +    SOME (x', _) => if intern_fixed ctxt x' = x then x' else x
   59.29    | NONE => x);
   59.30  
   59.31  fun markup_fixed ctxt x =