--- a/NEWS Wed Apr 01 19:17:41 2015 +0200
+++ b/NEWS Wed Apr 01 22:40:41 2015 +0200
@@ -6,6 +6,9 @@
*** General ***
+* Command 'experiment' opens an anonymous locale context with private
+naming policy.
+
* Structural composition of proof methods (meth1; meth2) in Isar
corresponds to (tac1 THEN_ALL_NEW tac2) in ML.
@@ -340,6 +343,14 @@
*** ML ***
+* Subtle change of name space policy: undeclared entries are now
+considered inaccessible, instead of accessible via the fully-qualified
+internal name. This mainly affects Name_Space.intern (and derivatives),
+which may produce an unexpected Long_Name.hidden prefix. Note that
+contempory applications use the strict Name_Space.check (and
+derivatives) instead, which is not affected by the change. Potential
+INCOMPATIBILITY in rare applications of Name_Space.intern.
+
* The main operations to certify logical entities are Thm.ctyp_of and
Thm.cterm_of with a local context; old-style global theory variants are
available as Thm.global_ctyp_of and Thm.global_cterm_of.
@@ -407,6 +418,8 @@
* The Isabelle tool "update_cartouches" changes theory files to use
cartouches instead of old-style {* verbatim *} or `alt_string` tokens.
+* The Isabelle tool "build" provides new options -k and -x.
+
New in Isabelle2014 (August 2014)
--- a/lib/Tools/build Wed Apr 01 19:17:41 2015 +0200
+++ b/lib/Tools/build Wed Apr 01 22:40:41 2015 +0200
@@ -34,11 +34,13 @@
echo " -d DIR include session directory"
echo " -g NAME select session group NAME"
echo " -j INT maximum number of parallel jobs (default 1)"
+ echo " -k KEYWORD check theory sources for conflicts with proposed keywords"
echo " -l list session source files"
echo " -n no build -- test dependencies only"
echo " -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)"
echo " -s system build mode: produce output in ISABELLE_HOME"
echo " -v verbose"
+ echo " -x SESSION exclude SESSION and all its descendants"
echo
echo " Build and manage Isabelle sessions, depending on implicit"
show_settings " "
@@ -68,13 +70,15 @@
declare -a INCLUDE_DIRS=()
declare -a SESSION_GROUPS=()
MAX_JOBS=1
+declare -a CHECK_KEYWORDS=()
LIST_FILES=false
NO_BUILD=false
eval "declare -a BUILD_OPTIONS=($ISABELLE_BUILD_OPTIONS)"
SYSTEM_MODE=false
VERBOSE=false
+declare -a EXCLUDE_SESSIONS=()
-while getopts "D:Rabcd:g:j:lno:sv" OPT
+while getopts "D:Rabcd:g:j:k:lno:svx:" OPT
do
case "$OPT" in
D)
@@ -102,6 +106,9 @@
check_number "$OPTARG"
MAX_JOBS="$OPTARG"
;;
+ k)
+ CHECK_KEYWORDS["${#CHECK_KEYWORDS[@]}"]="$OPTARG"
+ ;;
l)
LIST_FILES="true"
;;
@@ -117,6 +124,9 @@
v)
VERBOSE="true"
;;
+ x)
+ EXCLUDE_SESSIONS["${#EXCLUDE_SESSIONS[@]}"]="$OPTARG"
+ ;;
\?)
usage
;;
@@ -145,7 +155,8 @@
"$REQUIREMENTS" "$ALL_SESSIONS" "$BUILD_HEAP" "$CLEAN_BUILD" "$MAX_JOBS" \
"$LIST_FILES" "$NO_BUILD" "$SYSTEM_MODE" "$VERBOSE" \
"${INCLUDE_DIRS[@]}" $'\n' "${SELECT_DIRS[@]}" $'\n' \
- "${SESSION_GROUPS[@]}" $'\n' "${BUILD_OPTIONS[@]}" $'\n' "$@"
+ "${SESSION_GROUPS[@]}" $'\n' "${CHECK_KEYWORDS[@]}" $'\n' \
+ "${BUILD_OPTIONS[@]}" $'\n' "${EXCLUDE_SESSIONS[@]}" $'\n' "$@"
RC="$?"
if [ "$NO_BUILD" = false -a "$VERBOSE" = true ]; then
--- a/lib/Tools/scala Wed Apr 01 19:17:41 2015 +0200
+++ b/lib/Tools/scala Wed Apr 01 22:40:41 2015 +0200
@@ -6,6 +6,12 @@
isabelle_admin_build jars || exit $?
-isabelle_scala scala -Dfile.encoding=UTF-8 \
+declare -a JAVA_ARGS; eval "JAVA_ARGS=($ISABELLE_JAVA_SYSTEM_OPTIONS)"
+declare -a SCALA_ARGS=()
+for ARG in "${JAVA_ARGS[@]}"
+do
+ SCALA_ARGS["${#SCALA_ARGS[@]}"]="-J$ARG"
+done
+
+isabelle_scala scala "${SCALA_ARGS[@]}" \
-classpath "$(jvmpath "$ISABELLE_CLASSPATH")" "$@"
-
--- a/src/Doc/Implementation/Logic.thy Wed Apr 01 19:17:41 2015 +0200
+++ b/src/Doc/Implementation/Logic.thy Wed Apr 01 22:40:41 2015 +0200
@@ -982,7 +982,7 @@
theorem (in empty) false: False
using bad by blast
-ML \<open>@{assert} (Thm.extra_shyps @{thm false} = [@{sort empty}])\<close>
+ML_val \<open>@{assert} (Thm.extra_shyps @{thm false} = [@{sort empty}])\<close>
text \<open>Thanks to the inference kernel managing sort hypothesis
according to their logical significance, this example is merely an
--- a/src/Doc/Implementation/ML.thy Wed Apr 01 19:17:41 2015 +0200
+++ b/src/Doc/Implementation/ML.thy Wed Apr 01 22:40:41 2015 +0200
@@ -736,7 +736,7 @@
text %mlex \<open>The following artificial examples show how to produce
adhoc output of ML values for debugging purposes.\<close>
-ML \<open>
+ML_val \<open>
val x = 42;
val y = true;
@@ -928,7 +928,7 @@
list.
\<close>
-ML \<open>
+ML_val \<open>
val s =
Buffer.empty
|> Buffer.add "digits: "
@@ -1093,6 +1093,25 @@
"The frumious Bandersnatch!"]);
\<close>
+text \<open>
+ \medskip An alternative is to make a paragraph of freely-floating words as
+ follows.
+\<close>
+
+ML_command \<open>
+ warning (Pretty.string_of (Pretty.para
+ "Beware the Jabberwock, my son! \
+ \The jaws that bite, the claws that catch! \
+ \Beware the Jubjub Bird, and shun \
+ \The frumious Bandersnatch!"))
+\<close>
+
+text \<open>
+ This has advantages with variable window / popup sizes, but might make it
+ harder to search for message content systematically, e.g.\ by other tools or
+ by humans expecting the ``verse'' of a formal message in a fixed layout.
+\<close>
+
section \<open>Exceptions \label{sec:exceptions}\<close>
@@ -1551,7 +1570,7 @@
prevented.
\<close>
-ML \<open>
+ML_val \<open>
val items = [1, 2, 3, 4, 5, 6, 7, 8, 9, 10];
val list1 = fold cons items [];
@@ -1564,7 +1583,7 @@
text \<open>The subsequent example demonstrates how to \emph{merge} two
lists in a natural way.\<close>
-ML \<open>
+ML_val \<open>
fun merge_lists eq (xs, ys) = fold_rev (insert eq) ys xs;
\<close>
@@ -1817,7 +1836,7 @@
temporary file names.
\<close>
-ML \<open>
+ML_val \<open>
val tmp1 = File.tmp_path (Path.basic ("foo" ^ serial_string ()));
val tmp2 = File.tmp_path (Path.basic ("foo" ^ serial_string ()));
@{assert} (tmp1 <> tmp2);
@@ -1878,7 +1897,7 @@
positive integers that are unique over the runtime of the Isabelle
process:\<close>
-ML \<open>
+ML_val \<open>
local
val counter = Synchronized.var "counter" 0;
in
@@ -1888,9 +1907,7 @@
let val j = i + 1
in SOME (j, j) end);
end;
-\<close>
-
-ML \<open>
+
val a = next ();
val b = next ();
@{assert} (a <> b);
--- a/src/Doc/Implementation/Prelim.thy Wed Apr 01 19:17:41 2015 +0200
+++ b/src/Doc/Implementation/Prelim.thy Wed Apr 01 22:40:41 2015 +0200
@@ -501,6 +501,9 @@
value can be modified within Isar text like this:
\<close>
+experiment
+begin
+
declare [[show_types = false]]
-- \<open>declaration within (local) theory context\<close>
@@ -516,6 +519,8 @@
..
end
+end
+
text \<open>Configuration options that are not set explicitly hold a
default value that can depend on the application context. This
allows to retrieve the value from another slot within the context,
@@ -720,7 +725,7 @@
text %mlex \<open>The following simple examples demonstrate how to produce
fresh names from the initial @{ML Name.context}.\<close>
-ML \<open>
+ML_val \<open>
val list1 = Name.invent Name.context "a" 5;
@{assert} (list1 = ["a", "b", "c", "d", "e"]);
@@ -732,10 +737,10 @@
text \<open>\medskip The same works relatively to the formal context as
follows.\<close>
-locale ex = fixes a b c :: 'a
+experiment fixes a b c :: 'a
begin
-ML \<open>
+ML_val \<open>
val names = Variable.names_of @{context};
val list1 = Name.invent names "a" 5;
@@ -1043,7 +1048,7 @@
concrete binding inlined into the text:
\<close>
-ML \<open>Binding.pos_of @{binding here}\<close>
+ML_val \<open>Binding.pos_of @{binding here}\<close>
text \<open>\medskip That position can be also printed in a message as
follows:\<close>
--- a/src/Doc/Implementation/Proof.thy Wed Apr 01 19:17:41 2015 +0200
+++ b/src/Doc/Implementation/Proof.thy Wed Apr 01 22:40:41 2015 +0200
@@ -162,7 +162,7 @@
text %mlex \<open>The following example shows how to work with fixed term
and type parameters and with type-inference.\<close>
-ML \<open>
+ML_val \<open>
(*static compile-time context -- for testing only*)
val ctxt0 = @{context};
@@ -188,7 +188,7 @@
Alternatively, fixed parameters can be renamed explicitly as
follows:\<close>
-ML \<open>
+ML_val \<open>
val ctxt0 = @{context};
val ([x1, x2, x3], ctxt1) =
ctxt0 |> Variable.variant_fixes ["x", "x", "x"];
@@ -325,7 +325,7 @@
here for testing purposes.
\<close>
-ML \<open>
+ML_val \<open>
(*static compile-time context -- for testing only*)
val ctxt0 = @{context};
--- a/src/Doc/Implementation/Tactic.thy Wed Apr 01 19:17:41 2015 +0200
+++ b/src/Doc/Implementation/Tactic.thy Wed Apr 01 22:40:41 2015 +0200
@@ -709,7 +709,7 @@
\end{warn}
\<close>
-ML \<open>
+ML_val \<open>
(*BAD -- does not terminate!*)
fun REPEAT tac = (tac THEN REPEAT tac) ORELSE all_tac;
\<close>
--- a/src/Doc/Isar_Ref/Spec.thy Wed Apr 01 19:17:41 2015 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy Wed Apr 01 22:40:41 2015 +0200
@@ -501,6 +501,7 @@
text \<open>
\begin{matharray}{rcl}
@{command_def "locale"} & : & @{text "theory \<rightarrow> local_theory"} \\
+ @{command_def "experiment"} & : & @{text "theory \<rightarrow> local_theory"} \\
@{command_def "print_locale"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
@{command_def "print_locales"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
@{command_def "locale_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
@@ -513,6 +514,8 @@
@{rail \<open>
@@{command locale} @{syntax name} ('=' @{syntax locale})? @'begin'?
;
+ @@{command experiment} (@{syntax context_elem}*) @'begin'
+ ;
@@{command print_locale} '!'? @{syntax nameref}
;
@{syntax_def locale}: @{syntax context_elem}+ |
@@ -610,7 +613,12 @@
@{text "\<Longrightarrow>"} by @{text "\<longrightarrow>"} in HOL; see also
\secref{sec:object-logic}). Separate introduction rules @{text
loc_axioms.intro} and @{text loc.intro} are provided as well.
-
+
+ \item @{command experiment}~@{text exprs}~@{keyword "begin"} opens an
+ anonymous locale context with private naming policy. Specifications in its
+ body are inaccessible from outside. This is useful to perform experiments,
+ without polluting the name space.
+
\item @{command "print_locale"}~@{text "locale"} prints the
contents of the named locale. The command omits @{element "notes"}
elements by default. Use @{command "print_locale"}@{text "!"} to
--- a/src/Doc/System/Sessions.thy Wed Apr 01 19:17:41 2015 +0200
+++ b/src/Doc/System/Sessions.thy Wed Apr 01 22:40:41 2015 +0200
@@ -284,11 +284,13 @@
-d DIR include session directory
-g NAME select session group NAME
-j INT maximum number of parallel jobs (default 1)
+ -k KEYWORD check theory sources for conflicts with proposed keywords
-l list session source files
-n no build -- test dependencies only
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
-s system build mode: produce output in ISABELLE_HOME
-v verbose
+ -x SESSION exclude SESSION and all its descendants
Build and manage Isabelle sessions, depending on implicit
ISABELLE_BUILD_OPTIONS="..."
@@ -321,6 +323,10 @@
The build tool takes session dependencies into account: the set of
selected sessions is completed by including all ancestors.
+ \medskip One or more options @{verbatim "-x"}~@{text SESSION} specify
+ sessions to be excluded. All descendents of excluded sessions are removed
+ from the selection as specified above.
+
\medskip Option @{verbatim "-R"} reverses the selection in the sense
that it refers to its requirements: all ancestor sessions excluding
the original selection. This allows to prepare the stage for some
@@ -369,7 +375,12 @@
\medskip Option @{verbatim "-v"} increases the general level of
verbosity. Option @{verbatim "-l"} lists the source files that
contribute to a session.
-\<close>
+
+ \medskip Option @{verbatim "-k"} specifies a newly proposed keyword for
+ outer syntax (multiple uses allowed). The theory sources are checked for
+ conflicts wrt.\ this hypothetical change of syntax, e.g.\ to reveal
+ occurrences of identifiers that need to be quoted.\<close>
+
subsubsection \<open>Examples\<close>
--- a/src/FOL/ex/Locale_Test/Locale_Test1.thy Wed Apr 01 19:17:41 2015 +0200
+++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy Wed Apr 01 22:40:41 2015 +0200
@@ -775,7 +775,7 @@
locale container
begin
-interpretation private!: roundup True by unfold_locales rule
+interpretation "private"!: roundup True by unfold_locales rule
lemmas true_copy = private.true
end
--- a/src/HOL/Bali/WellForm.thy Wed Apr 01 19:17:41 2015 +0200
+++ b/src/HOL/Bali/WellForm.thy Wed Apr 01 22:40:41 2015 +0200
@@ -1979,7 +1979,7 @@
lemma dynmethd_Object:
assumes statM: "methd G Object sig = Some statM" and
- private: "accmodi statM = Private" and
+ "private": "accmodi statM = Private" and
is_cls_C: "is_class G C" and
wf: "wf_prog G"
shows "dynmethd G Object C sig = Some statM"
@@ -1992,13 +1992,13 @@
from wf
have is_cls_Obj: "is_class G Object"
by simp
- from statM subclseq is_cls_Obj ws private
+ from statM subclseq is_cls_Obj ws "private"
show ?thesis
proof (cases rule: dynmethd_cases)
case Static then show ?thesis .
next
case Overrides
- with private show ?thesis
+ with "private" show ?thesis
by (auto dest: no_Private_override)
qed
qed
--- a/src/HOL/Library/Code_Test.thy Wed Apr 01 19:17:41 2015 +0200
+++ b/src/HOL/Library/Code_Test.thy Wed Apr 01 22:40:41 2015 +0200
@@ -64,7 +64,7 @@
by(cases x y rule: xml_tree.exhaust[case_product xml_tree.exhaust])(simp)
context begin
-local_setup {* Local_Theory.map_naming (Name_Space.mandatory_path "xml") *}
+local_setup {* Local_Theory.map_background_naming (Name_Space.mandatory_path "xml") *}
type_synonym attributes = "(String.literal \<times> String.literal) list"
type_synonym body = "xml_tree list"
--- a/src/HOL/Nominal/nominal_datatype.ML Wed Apr 01 19:17:41 2015 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML Wed Apr 01 22:40:41 2015 +0200
@@ -529,7 +529,7 @@
val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy4) =
thy3
- |> Sign.map_naming Name_Space.concealed
+ |> Sign.concealed
|> Inductive.add_inductive_global
{quiet_mode = false, verbose = false, alt_name = Binding.name big_rep_name,
coind = false, no_elim = true, no_ind = false, skip_mono = true}
@@ -1505,7 +1505,7 @@
val ({intrs = rec_intrs, elims = rec_elims, raw_induct = rec_induct, ...}, thy11) =
thy10
- |> Sign.map_naming Name_Space.concealed
+ |> Sign.concealed
|> Inductive.add_inductive_global
{quiet_mode = #quiet config, verbose = false, alt_name = Binding.name big_rec_name,
coind = false, no_elim = false, no_ind = false, skip_mono = true}
--- a/src/HOL/Product_Type.thy Wed Apr 01 19:17:41 2015 +0200
+++ b/src/HOL/Product_Type.thy Wed Apr 01 22:40:41 2015 +0200
@@ -988,7 +988,7 @@
context
begin
-local_setup {* Local_Theory.map_naming (Name_Space.mandatory_path "prod") *}
+local_setup {* Local_Theory.map_background_naming (Name_Space.mandatory_path "prod") *}
definition swap :: "'a \<times> 'b \<Rightarrow> 'b \<times> 'a"
where
--- a/src/HOL/ROOT Wed Apr 01 19:17:41 2015 +0200
+++ b/src/HOL/ROOT Wed Apr 01 22:40:41 2015 +0200
@@ -706,7 +706,7 @@
"ex/Measure_Not_CCC"
document_files "root.tex"
-session "HOL-Nominal" (main) in Nominal = HOL +
+session "HOL-Nominal" in Nominal = HOL +
options [document = false]
theories Nominal
--- a/src/HOL/Statespace/state_space.ML Wed Apr 01 19:17:41 2015 +0200
+++ b/src/HOL/Statespace/state_space.ML Wed Apr 01 22:40:41 2015 +0200
@@ -173,7 +173,7 @@
fun mk_free ctxt name =
if Variable.is_fixed ctxt name orelse Variable.is_declared ctxt name
then
- let val n' = Variable.intern_fixed ctxt name
+ let val n' = Variable.intern_fixed ctxt name |> perhaps Long_Name.dest_hidden;
in SOME (Free (n', Proof_Context.infer_type ctxt (n', dummyT))) end
else NONE
--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy Wed Apr 01 19:17:41 2015 +0200
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy Wed Apr 01 22:40:41 2015 +0200
@@ -737,16 +737,17 @@
bnd_def
val thm =
- if Name_Space.defined_entry (Theory.axiom_space thy) def_name then
- Thm.axiom thy def_name
- else
- if is_none prob_name_opt then
- (*This mode is for testing, so we can be a bit
- looser with theories*)
- Thm.add_axiom_global (bnd_name, conclusion) thy
- |> fst |> snd
- else
- raise (NO_SKOLEM_DEF (def_name, bnd_name, conclusion))
+ (case try (Thm.axiom thy) def_name of
+ SOME thm => thm
+ | NONE =>
+ if is_none prob_name_opt then
+ (*This mode is for testing, so we can be a bit
+ looser with theories*)
+ (* FIXME bad theory context!? *)
+ Thm.add_axiom_global (bnd_name, conclusion) thy
+ |> fst |> snd
+ else
+ raise (NO_SKOLEM_DEF (def_name, bnd_name, conclusion)))
in
rtac (Drule.export_without_context thm) i st
end
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Wed Apr 01 19:17:41 2015 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Wed Apr 01 22:40:41 2015 +0200
@@ -396,9 +396,8 @@
fun make_class clas = class_prefix ^ ascii_of clas
fun new_skolem_var_name_of_const s =
- let val ss = s |> space_explode Long_Name.separator in
- nth ss (length ss - 2)
- end
+ let val ss = Long_Name.explode s
+ in nth ss (length ss - 2) end
(* These are ignored anyway by the relevance filter (unless they appear in
higher-order places) but not by the monomorphizer. *)
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Wed Apr 01 19:17:41 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Wed Apr 01 22:40:41 2015 +0200
@@ -414,9 +414,8 @@
val ps = map (`Long_Name.base_name) names;
val dups = Library.duplicates (op =) (map fst ps);
fun underscore s =
- let val ss = space_explode Long_Name.separator s in
- space_implode "_" (drop (length ss - 2) ss)
- end;
+ let val ss = Long_Name.explode s
+ in space_implode "_" (drop (length ss - 2) ss) end;
in
map (fn (base, full) => if member (op =) dups base then underscore full else base) ps
|> Name.variant_list []
--- a/src/HOL/Tools/BNF/bnf_util.ML Wed Apr 01 19:17:41 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_util.ML Wed Apr 01 22:40:41 2015 +0200
@@ -145,9 +145,9 @@
val b' = fold_rev Binding.prefix_name (map (suffix "_" o fst) (Binding.path_of b)) b;
val ((name, info), (lthy, lthy_old)) =
lthy
- |> Local_Theory.concealed
+ |> Proof_Context.concealed
|> Typedef.add_typedef true (b', Ts, mx) set opt_morphs tac
- ||> Local_Theory.restore_naming lthy
+ ||> Proof_Context.restore_naming lthy
||> `Local_Theory.restore;
val phi = Proof_Context.export_morphism lthy_old lthy;
in
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML Wed Apr 01 19:17:41 2015 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML Wed Apr 01 22:40:41 2015 +0200
@@ -231,7 +231,7 @@
| name_noted_thms qualifier base ((local_name, thms) :: noted) =
if Long_Name.base_name local_name = base then
(local_name,
- map_index (uncurry (fn j => Thm.name_derivation (qualifier ^ Long_Name.separator ^ base ^
+ map_index (uncurry (fn j => Thm.name_derivation (Long_Name.append qualifier base ^
(if can the_single thms then "" else "_" ^ string_of_int (j + 1))))) thms) :: noted
else
((local_name, thms) :: name_noted_thms qualifier base noted);
--- a/src/HOL/Tools/Function/function_core.ML Wed Apr 01 19:17:41 2015 +0200
+++ b/src/HOL/Tools/Function/function_core.ML Wed Apr 01 22:40:41 2015 +0200
@@ -445,7 +445,7 @@
let
val ({intrs = intrs_gen, elims = [elim_gen], preds = [ Rdef ], induct, ...}, lthy) =
lthy
- |> Local_Theory.concealed
+ |> Proof_Context.concealed
|> Inductive.add_inductive_i
{quiet_mode = true,
verbose = ! trace,
@@ -458,7 +458,7 @@
[] (* no parameters *)
(map (fn t => (Attrib.empty_binding, t)) intrs) (* intro rules *)
[] (* no special monos *)
- ||> Local_Theory.restore_naming lthy
+ ||> Proof_Context.restore_naming lthy
fun requantify orig_intro thm =
let
--- a/src/HOL/Tools/Metis/metis_generate.ML Wed Apr 01 19:17:41 2015 +0200
+++ b/src/HOL/Tools/Metis/metis_generate.ML Wed Apr 01 22:40:41 2015 +0200
@@ -66,8 +66,7 @@
else metis_ad_hoc_type_tag, true))]
fun old_skolem_const_name i j num_T_args =
- old_skolem_const_prefix ^ Long_Name.separator ^
- (space_implode Long_Name.separator (map string_of_int [i, j, num_T_args]))
+ Long_Name.implode (old_skolem_const_prefix :: map string_of_int [i, j, num_T_args])
fun conceal_old_skolem_terms i old_skolems t =
if exists_Const (curry (op =) @{const_name Meson.skolem} o fst) t then
--- a/src/HOL/Tools/Old_Datatype/old_datatype.ML Wed Apr 01 19:17:41 2015 +0200
+++ b/src/HOL/Tools/Old_Datatype/old_datatype.ML Wed Apr 01 22:40:41 2015 +0200
@@ -172,7 +172,7 @@
val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy2) =
thy1
- |> Sign.map_naming Name_Space.concealed
+ |> Sign.concealed
|> Inductive.add_inductive_global
{quiet_mode = #quiet config, verbose = false, alt_name = Binding.name big_rec_name,
coind = false, no_elim = true, no_ind = false, skip_mono = true}
--- a/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML Wed Apr 01 19:17:41 2015 +0200
+++ b/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML Wed Apr 01 22:40:41 2015 +0200
@@ -146,7 +146,7 @@
val ({intrs = rec_intrs, elims = rec_elims, ...}, thy1) =
thy0
- |> Sign.map_naming Name_Space.concealed
+ |> Sign.concealed
|> Inductive.add_inductive_global
{quiet_mode = #quiet config, verbose = false, alt_name = Binding.name big_rec_name',
coind = false, no_elim = false, no_ind = true, skip_mono = true}
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Wed Apr 01 19:17:41 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Wed Apr 01 22:40:41 2015 +0200
@@ -476,7 +476,7 @@
fun add_facts global foldx facts =
foldx (fn (name0, ths) => fn accum =>
if name0 <> "" andalso
- (Long_Name.is_hidden (Facts.intern facts name0) orelse
+ (is_some (Long_Name.dest_hidden (Facts.intern facts name0)) orelse
((Facts.is_concealed facts name0 orelse
(not generous andalso is_blacklisted_or_something name0)) andalso
forall (not o member Thm.eq_thm_prop add_ths) ths)) then
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Wed Apr 01 19:17:41 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Wed Apr 01 22:40:41 2015 +0200
@@ -737,8 +737,6 @@
(*** Isabelle helpers ***)
-val local_prefix = "local" ^ Long_Name.separator
-
fun elided_backquote_thm threshold th =
elide_string threshold (backquote_thm (Proof_Context.init_global (Thm.theory_of_thm th)) th)
@@ -748,10 +746,8 @@
if Thm.has_name_hint th then
let val hint = Thm.get_name_hint th in
(* There must be a better way to detect local facts. *)
- (case try (unprefix local_prefix) hint of
- SOME suf =>
- thy_name_of_thm th ^ Long_Name.separator ^ suf ^ Long_Name.separator ^
- elided_backquote_thm 50 th
+ (case Long_Name.dest_local hint of
+ SOME suf => Long_Name.implode [thy_name_of_thm th, suf, elided_backquote_thm 50 th]
| NONE => hint)
end
else
@@ -886,7 +882,7 @@
| pattify_term _ _ (Free (s, T)) =
maybe_singleton_str pat_var_prefix (crude_str_of_typ T)
|> (if member (op =) fixes s then
- cons (free_feature_of (massage_long_name (thy_name ^ Long_Name.separator ^ s)))
+ cons (free_feature_of (massage_long_name (Long_Name.append thy_name s)))
else
I)
| pattify_term _ _ (Var (_, T)) = maybe_singleton_str pat_var_prefix (crude_str_of_typ T)
--- a/src/HOL/Tools/inductive.ML Wed Apr 01 19:17:41 2015 +0200
+++ b/src/HOL/Tools/inductive.ML Wed Apr 01 22:40:41 2015 +0200
@@ -843,13 +843,13 @@
val is_auxiliary = length cs >= 2;
val ((rec_const, (_, fp_def)), lthy') = lthy
- |> is_auxiliary ? Local_Theory.concealed
+ |> is_auxiliary ? Proof_Context.concealed
|> Local_Theory.define
((rec_name, case cnames_syn of [(_, syn)] => syn | _ => NoSyn),
((Binding.concealed (Thm.def_binding rec_name), @{attributes [nitpick_unfold]}),
fold_rev lambda params
(Const (fp_name, (predT --> predT) --> predT) $ fp_fun)))
- ||> is_auxiliary ? Local_Theory.restore_naming lthy;
+ ||> Proof_Context.restore_naming lthy;
val fp_def' =
Simplifier.rewrite (put_simpset HOL_basic_ss lthy' addsimps [fp_def])
(Thm.cterm_of lthy' (list_comb (rec_const, params)));
--- a/src/HOL/Tools/inductive_set.ML Wed Apr 01 19:17:41 2015 +0200
+++ b/src/HOL/Tools/inductive_set.ML Wed Apr 01 22:40:41 2015 +0200
@@ -488,13 +488,13 @@
(* define inductive sets using previously defined predicates *)
val (defs, lthy2) = lthy1
- |> Local_Theory.concealed (* FIXME ?? *)
+ |> Proof_Context.concealed (* FIXME ?? *)
|> fold_map Local_Theory.define
(map (fn (((c, syn), (fs, U, _)), p) => ((c, syn), ((Thm.def_binding c, []),
fold_rev lambda params (HOLogic.Collect_const U $
HOLogic.mk_psplits fs U HOLogic.boolT (list_comb (p, params3))))))
(cnames_syn ~~ cs_info ~~ preds))
- ||> Local_Theory.restore_naming lthy1;
+ ||> Proof_Context.restore_naming lthy1;
(* prove theorems for converting predicate to set notation *)
val lthy3 = fold
--- a/src/HOL/Tools/typedef.ML Wed Apr 01 19:17:41 2015 +0200
+++ b/src/HOL/Tools/typedef.ML Wed Apr 01 22:40:41 2015 +0200
@@ -81,10 +81,10 @@
Typedef_Plugin.interpretation typedef_plugin
(fn name => fn lthy =>
lthy
- |> Local_Theory.map_naming
+ |> Local_Theory.map_background_naming
(Name_Space.root_path #> Name_Space.add_path (Long_Name.qualifier name))
|> f name
- |> Local_Theory.restore_naming lthy);
+ |> Local_Theory.restore_background_naming lthy);
(* primitive typedef axiomatization -- for fresh typedecl *)
--- a/src/Pure/General/binding.ML Wed Apr 01 19:17:41 2015 +0200
+++ b/src/Pure/General/binding.ML Wed Apr 01 22:40:41 2015 +0200
@@ -9,8 +9,9 @@
signature BINDING =
sig
+ eqtype scope
+ val new_scope: unit -> scope
eqtype binding
- val dest: binding -> {private: bool, concealed: bool, path: (string * bool) list, name: bstring}
val path_of: binding -> (string * bool) list
val make: bstring * Position.T -> binding
val pos_of: binding -> Position.T
@@ -29,13 +30,16 @@
val prefix_of: binding -> (string * bool) list
val map_prefix: ((string * bool) list -> (string * bool) list) -> binding -> binding
val prefix: bool -> string -> binding -> binding
- val private: binding -> binding
+ val private: scope -> binding -> binding
+ val private_default: scope option -> binding -> binding
val concealed: binding -> binding
val pretty: binding -> Pretty.T
val print: binding -> string
val pp: binding -> Pretty.T
val bad: binding -> string
val check: binding -> unit
+ val name_spec: scope list -> (string * bool) list -> binding ->
+ {accessible: bool, concealed: bool, spec: (string * bool) list}
end;
structure Binding: BINDING =
@@ -43,10 +47,17 @@
(** representation **)
-(* datatype *)
+(* scope of private entries *)
+
+datatype scope = Scope of serial;
+
+fun new_scope () = Scope (serial ());
+
+
+(* binding *)
datatype binding = Binding of
- {private: bool, (*entry is strictly private -- no name space accesses*)
+ {private: scope option, (*entry is strictly private within its scope*)
concealed: bool, (*entry is for foundational purposes -- please ignore*)
prefix: (string * bool) list, (*system prefix*)
qualifier: (string * bool) list, (*user qualifier*)
@@ -60,10 +71,7 @@
fun map_binding f (Binding {private, concealed, prefix, qualifier, name, pos}) =
make_binding (f (private, concealed, prefix, qualifier, name, pos));
-fun dest (Binding {private, concealed, prefix, qualifier, name, ...}) =
- {private = private, concealed = concealed, path = prefix @ qualifier, name = name};
-
-val path_of = #path o dest;
+fun path_of (Binding {prefix, qualifier, ...}) = prefix @ qualifier;
@@ -71,7 +79,7 @@
(* name and position *)
-fun make (name, pos) = make_binding (false, false, [], [], name, pos);
+fun make (name, pos) = make_binding (NONE, false, [], [], name, pos);
fun pos_of (Binding {pos, ...}) = pos;
fun set_pos pos =
@@ -109,7 +117,7 @@
fun qualified_name "" = empty
| qualified_name s =
let val (qualifier, name) = split_last (Long_Name.explode s)
- in make_binding (false, false, [], map (rpair false) qualifier, name, Position.none) end;
+ in make_binding (NONE, false, [], map (rpair false) qualifier, name, Position.none) end;
(* system prefix *)
@@ -126,9 +134,13 @@
(* visibility flags *)
-val private =
+fun private scope =
map_binding (fn (_, concealed, prefix, qualifier, name, pos) =>
- (true, concealed, prefix, qualifier, name, pos));
+ (SOME scope, concealed, prefix, qualifier, name, pos));
+
+fun private_default private' =
+ map_binding (fn (private, concealed, prefix, qualifier, name, pos) =>
+ (if is_some private then private else private', concealed, prefix, qualifier, name, pos));
val concealed =
map_binding (fn (private, _, prefix, qualifier, name, pos) =>
@@ -157,6 +169,31 @@
if Symbol_Pos.is_identifier (name_of binding) then ()
else legacy_feature (bad binding);
+
+
+(** resulting name_spec **)
+
+val bad_specs = ["", "??", "__"];
+
+fun name_spec scopes path binding =
+ let
+ val Binding {private, concealed, prefix, qualifier, name, ...} = binding;
+ val _ = Long_Name.is_qualified name andalso error (bad binding);
+
+ val accessible =
+ (case private of
+ NONE => true
+ | SOME scope => member (op =) scopes scope);
+
+ val spec1 =
+ maps (fn (a, b) => map (rpair b) (Long_Name.explode a)) (path @ prefix @ qualifier);
+ val spec2 = if name = "" then [] else [(name, true)];
+ val spec = spec1 @ spec2;
+ val _ =
+ exists (fn (a, _) => member (op =) bad_specs a orelse exists_string (fn s => s = "\"") a) spec
+ andalso error (bad binding);
+ in {accessible = accessible, concealed = concealed, spec = if null spec2 then [] else spec} end;
+
end;
type binding = Binding.binding;
--- a/src/Pure/General/long_name.ML Wed Apr 01 19:17:41 2015 +0200
+++ b/src/Pure/General/long_name.ML Wed Apr 01 22:40:41 2015 +0200
@@ -9,9 +9,9 @@
val separator: string
val is_qualified: string -> bool
val hidden: string -> string
- val is_hidden: string -> bool
+ val dest_hidden: string -> string option
val localN: string
- val is_local: string -> bool
+ val dest_local: string -> string option
val implode: string list -> string
val explode: string -> string list
val append: string -> string -> string
@@ -29,11 +29,11 @@
val is_qualified = exists_string (fn s => s = separator);
-fun hidden name = "??." ^ name;
-val is_hidden = String.isPrefix "??.";
+val hidden = prefix "??.";
+val dest_hidden = try (unprefix "??.");
val localN = "local";
-val is_local = String.isPrefix "local.";
+val dest_local = try (unprefix "local.");
val implode = space_implode separator;
val explode = space_explode separator;
--- a/src/Pure/General/name_space.ML Wed Apr 01 19:17:41 2015 +0200
+++ b/src/Pure/General/name_space.ML Wed Apr 01 22:40:41 2015 +0200
@@ -12,11 +12,10 @@
type T
val empty: string -> T
val kind_of: T -> string
- val defined_entry: T -> string -> bool
+ val markup: T -> string -> Markup.T
val the_entry: T -> string ->
{concealed: bool, group: serial option, theory_name: string, pos: Position.T, serial: serial}
val entry_ord: T -> string * string -> order
- val markup: T -> string -> Markup.T
val is_concealed: T -> string -> bool
val intern: T -> xstring -> string
val names_long_raw: Config.raw
@@ -33,7 +32,9 @@
val completion: Context.generic -> T -> xstring * Position.T -> Completion.T
val merge: T * T -> T
type naming
- val private: naming -> naming
+ val get_scope: naming -> Binding.scope option
+ val new_scope: naming -> Binding.scope * naming
+ val private: Binding.scope -> naming -> naming
val concealed: naming -> naming
val get_group: naming -> serial option
val set_group: serial option -> naming -> naming
@@ -47,6 +48,7 @@
val qualified_path: bool -> binding -> naming -> naming
val global_naming: naming
val local_naming: naming
+ val transform_naming: naming -> naming -> naming
val transform_binding: naming -> binding -> binding
val full_name: naming -> binding -> string
val base_name: binding -> string
@@ -62,6 +64,8 @@
val check_reports: Context.generic -> 'a table ->
xstring * Position.T list -> (string * Position.report list) * 'a
val check: Context.generic -> 'a table -> xstring * Position.T -> string * 'a
+ val defined: 'a table -> string -> bool
+ val lookup: 'a table -> string -> 'a option
val lookup_key: 'a table -> string -> (string * 'a) option
val get: 'a table -> string -> 'a
val define: Context.generic -> bool -> binding * 'a -> 'a table -> string * 'a table
@@ -105,12 +109,10 @@
error ("Duplicate " ^ plain_words kind ^ " declaration " ^
print_entry_ref kind entry1 ^ " vs. " ^ print_entry_ref kind entry2 ^ Position.here pos);
-fun undefined kind name = "Undefined " ^ plain_words kind ^ ": " ^ quote name;
-
(* internal names *)
-type internals = (string list * string list) Change_Table.T; (*xname -> visible, hidden*)
+type internals = (string list * string list) Change_Table.T;
fun map_internals f xname : internals -> internals =
Change_Table.map_default (xname, ([], [])) f;
@@ -119,14 +121,15 @@
fun del_name_extra name =
map_internals (apfst (fn [] => [] | x :: xs => x :: remove (op =) name xs));
val add_name = map_internals o apfst o update (op =);
-val add_name' = map_internals o apsnd o update (op =);
+fun hide_name name = map_internals (apsnd (update (op =) name)) name;
(* datatype T *)
datatype T =
Name_Space of
- {kind: string, internals: internals,
+ {kind: string,
+ internals: internals, (*xname -> visible, hidden*)
entries: (xstring list * entry) Change_Table.T}; (*name -> externals, entry*)
fun make_name_space (kind, internals, entries) =
@@ -146,36 +149,46 @@
fun kind_of (Name_Space {kind, ...}) = kind;
-fun defined_entry (Name_Space {entries, ...}) = Change_Table.defined entries;
-
-fun the_entry (Name_Space {kind, entries, ...}) name =
- (case Change_Table.lookup entries name of
- NONE => error (undefined kind name)
- | SOME (_, entry) => entry);
-
-fun entry_ord space = int_ord o apply2 (#serial o the_entry space);
-
fun markup (Name_Space {kind, entries, ...}) name =
(case Change_Table.lookup entries name of
NONE => Markup.intensify
| SOME (_, entry) => entry_markup false kind (name, entry));
+fun undefined (space as Name_Space {kind, entries, ...}) bad =
+ let
+ val (prfx, sfx) =
+ (case Long_Name.dest_hidden bad of
+ SOME name =>
+ if Change_Table.defined entries name
+ then ("Inaccessible", Markup.markup (markup space name) (quote name))
+ else ("Undefined", quote name)
+ | NONE => ("Undefined", quote bad));
+ in prfx ^ " " ^ plain_words kind ^ ": " ^ sfx end;
+
+fun the_entry (space as Name_Space {entries, ...}) name =
+ (case Change_Table.lookup entries name of
+ NONE => error (undefined space name)
+ | SOME (_, entry) => entry);
+
+fun entry_ord space = int_ord o apply2 (#serial o the_entry space);
+
fun is_concealed space name = #concealed (the_entry space name);
-(* name accesses *)
+(* intern *)
-fun lookup (Name_Space {internals, ...}) xname =
- (case Change_Table.lookup internals xname of
- NONE => (xname, true)
- | SOME ([], []) => (xname, true)
- | SOME ([name], _) => (name, true)
- | SOME (name :: _, _) => (name, false)
- | SOME ([], name' :: _) => (Long_Name.hidden name', true));
+fun intern' (Name_Space {internals, ...}) xname =
+ (case the_default ([], []) (Change_Table.lookup internals xname) of
+ ([name], _) => (name, true)
+ | (name :: _, _) => (name, false)
+ | ([], []) => (Long_Name.hidden xname, true)
+ | ([], name' :: _) => (Long_Name.hidden name', true));
+
+val intern = #1 oo intern';
fun get_accesses (Name_Space {entries, ...}) name =
(case Change_Table.lookup entries name of
- NONE => [name]
+ NONE => []
| SOME (externals, _) => externals);
fun valid_accesses (Name_Space {internals, ...}) name =
@@ -183,11 +196,6 @@
if not (null names) andalso hd names = name then cons xname else I) internals [];
-(* intern *)
-
-fun intern space xname = #1 (lookup space xname);
-
-
(* extern *)
val names_long_raw = Config.declare_option ("names_long", @{here});
@@ -206,7 +214,7 @@
val names_unique = Config.get ctxt names_unique;
fun valid require_unique xname =
- let val (name', is_unique) = lookup space xname
+ let val (name', is_unique) = intern' space xname
in name = name' andalso (not require_unique orelse is_unique) end;
fun ext [] = if valid false name then name else Long_Name.hidden name
@@ -236,7 +244,7 @@
Completion.make (xname, pos) (fn completed =>
let
fun result_ord ((xname1, (_, name1)), (xname2, (_, name2))) =
- (case bool_ord (apply2 Long_Name.is_local (name2, name1)) of
+ (case bool_ord (apply2 (is_some o Long_Name.dest_local) (name2, name1)) of
EQUAL =>
(case int_ord (apply2 Long_Name.qualification (xname1, xname2)) of
EQUAL => string_ord (xname1, xname2)
@@ -284,41 +292,54 @@
(* datatype naming *)
datatype naming = Naming of
- {private: bool,
+ {scopes: Binding.scope list,
+ private: Binding.scope option,
concealed: bool,
group: serial option,
theory_name: string,
path: (string * bool) list};
-fun make_naming (private, concealed, group, theory_name, path) =
- Naming {private = private, concealed = concealed, group = group,
- theory_name = theory_name, path = path};
+fun make_naming (scopes, private, concealed, group, theory_name, path) =
+ Naming {scopes = scopes, private = private, concealed = concealed,
+ group = group, theory_name = theory_name, path = path};
-fun map_naming f (Naming {private, concealed, group, theory_name, path}) =
- make_naming (f (private, concealed, group, theory_name, path));
+fun map_naming f (Naming {scopes, private, concealed, group, theory_name, path}) =
+ make_naming (f (scopes, private, concealed, group, theory_name, path));
-fun map_path f = map_naming (fn (private, concealed, group, theory_name, path) =>
- (private, concealed, group, theory_name, f path));
+fun map_path f = map_naming (fn (scopes, private, concealed, group, theory_name, path) =>
+ (scopes, private, concealed, group, theory_name, f path));
-val private = map_naming (fn (_, concealed, group, theory_name, path) =>
- (true, concealed, group, theory_name, path));
+fun get_scopes (Naming {scopes, ...}) = scopes;
+val get_scope = try hd o get_scopes;
-val concealed = map_naming (fn (private, _, group, theory_name, path) =>
- (private, true, group, theory_name, path));
+fun new_scope naming =
+ let
+ val scope = Binding.new_scope ();
+ val naming' =
+ naming |> map_naming (fn (scopes, private, concealed, group, theory_name, path) =>
+ (scope :: scopes, private, concealed, group, theory_name, path));
+ in (scope, naming') end;
-fun set_theory_name theory_name = map_naming (fn (private, concealed, group, _, path) =>
- (private, concealed, group, theory_name, path));
+fun private scope = map_naming (fn (scopes, _, concealed, group, theory_name, path) =>
+ (scopes, SOME scope, concealed, group, theory_name, path));
+val concealed = map_naming (fn (scopes, private, _, group, theory_name, path) =>
+ (scopes, private, true, group, theory_name, path));
+
+fun set_theory_name theory_name = map_naming (fn (scopes, private, concealed, group, _, path) =>
+ (scopes, private, concealed, group, theory_name, path));
fun get_group (Naming {group, ...}) = group;
-fun set_group group = map_naming (fn (private, concealed, _, theory_name, path) =>
- (private, concealed, group, theory_name, path));
+fun set_group group = map_naming (fn (scopes, private, concealed, _, theory_name, path) =>
+ (scopes, private, concealed, group, theory_name, path));
fun new_group naming = set_group (SOME (serial ())) naming;
val reset_group = set_group NONE;
+fun get_path (Naming {path, ...}) = path;
+
fun add_path elems = map_path (fn path => path @ [(elems, false)]);
val root_path = map_path (fn _ => []);
val parent_path = map_path (perhaps (try (#1 o split_last)));
@@ -327,33 +348,25 @@
fun qualified_path mandatory binding = map_path (fn path =>
path @ Binding.path_of (Binding.qualified mandatory "" binding));
-val global_naming = make_naming (false, false, NONE, "", []);
+val global_naming = make_naming ([], NONE, false, NONE, "", []);
val local_naming = global_naming |> add_path Long_Name.localN;
+(* visibility flags *)
+
+fun transform_naming (Naming {private = private', concealed = concealed', ...}) =
+ fold private (the_list private') #>
+ concealed' ? concealed;
+
+fun transform_binding (Naming {private, concealed, ...}) =
+ Binding.private_default private #>
+ concealed ? Binding.concealed;
+
+
(* full name *)
-fun err_bad binding = error (Binding.bad binding);
-
-fun transform_binding (Naming {private, concealed, ...}) =
- private ? Binding.private #>
- concealed ? Binding.concealed;
-
-val bad_specs = ["", "??", "__"];
-
-fun name_spec (naming as Naming {path = path1, ...}) raw_binding =
- let
- val binding = transform_binding naming raw_binding;
- val {private, concealed, path = path2, name} = Binding.dest binding;
- val _ = Long_Name.is_qualified name andalso err_bad binding;
-
- val spec1 = maps (fn (a, b) => map (rpair b) (Long_Name.explode a)) (path1 @ path2);
- val spec2 = if name = "" then [] else [(name, true)];
- val spec = spec1 @ spec2;
- val _ =
- exists (fn (a, _) => member (op =) bad_specs a orelse exists_string (fn s => s = "\"") a) spec
- andalso err_bad binding;
- in {private = private, concealed = concealed, spec = if null spec2 then [] else spec} end;
+fun name_spec naming binding =
+ Binding.name_spec (get_scopes naming) (get_path naming) (transform_binding naming binding);
fun full_name naming =
name_spec naming #> #spec #> map #1 #> Long_Name.implode;
@@ -374,7 +387,7 @@
fun accesses naming binding =
(case name_spec naming binding of
- {private = true, ...} => ([], [])
+ {accessible = false, ...} => ([], [])
| {spec, ...} =>
let
val sfxs = mandatory_suffixes spec;
@@ -387,10 +400,10 @@
fun hide fully name space =
space |> map_name_space (fn (kind, internals, entries) =>
let
- val _ = Change_Table.defined entries name orelse error (undefined kind name);
+ val _ = the_entry space name;
val names = valid_accesses space name;
val internals' = internals
- |> add_name' name name
+ |> hide_name name
|> fold (del_name name)
(if fully then names else inter (op =) [Long_Name.base_name name] names)
|> fold (del_name_extra name) (get_accesses space name);
@@ -402,7 +415,7 @@
fun alias naming binding name space =
space |> map_name_space (fn (kind, internals, entries) =>
let
- val _ = Change_Table.defined entries name orelse error (undefined kind name);
+ val _ = the_entry space name;
val (accs, accs') = accesses naming binding;
val internals' = internals |> fold (add_name name) accs;
val entries' = entries
@@ -446,7 +459,7 @@
val (accs, accs') = accesses naming binding;
val name = Long_Name.implode (map fst spec);
- val _ = name = "" andalso err_bad binding;
+ val _ = name = "" andalso error (Binding.bad binding);
val (proper_pos, pos) = Position.default (Binding.pos_of binding);
val entry =
@@ -498,7 +511,7 @@
let
val completions = map (fn pos => completion context space (xname, pos)) ps;
in
- error (undefined (kind_of space) name ^ Position.here_list ps ^
+ error (undefined space name ^ Position.here_list ps ^
Markup.markup_report (implode (map Completion.reported_text completions)))
end)
end;
@@ -509,12 +522,14 @@
val _ = Position.reports reports;
in (name, x) end;
+fun defined (Table (_, tab)) name = Change_Table.defined tab name;
+fun lookup (Table (_, tab)) name = Change_Table.lookup tab name;
fun lookup_key (Table (_, tab)) name = Change_Table.lookup_key tab name;
fun get table name =
(case lookup_key table name of
SOME (_, x) => x
- | NONE => error (undefined (kind_of (space_of_table table)) name));
+ | NONE => error (undefined (space_of_table table) name));
fun define context strict (binding, x) (Table (space, tab)) =
let
--- a/src/Pure/Isar/bundle.ML Wed Apr 01 19:17:41 2015 +0200
+++ b/src/Pure/Isar/bundle.ML Wed Apr 01 22:40:41 2015 +0200
@@ -20,9 +20,10 @@
val include_cmd: (xstring * Position.T) list -> Proof.state -> Proof.state
val including: string list -> Proof.state -> Proof.state
val including_cmd: (xstring * Position.T) list -> Proof.state -> Proof.state
- val context: string list -> Element.context_i list -> generic_theory -> local_theory
+ val context: string list -> Element.context_i list ->
+ generic_theory -> Binding.scope * local_theory
val context_cmd: (xstring * Position.T) list -> Element.context list ->
- generic_theory -> local_theory
+ generic_theory -> Binding.scope * local_theory
val print_bundles: Proof.context -> unit
end;
@@ -97,8 +98,8 @@
|> gen_includes get raw_incls
|> prep_decl ([], []) I raw_elems;
in
- lthy' |> Local_Theory.open_target
- (Local_Theory.naming_of lthy) (Local_Theory.operations_of lthy) after_close
+ lthy' |> Local_Theory.init_target
+ (Local_Theory.background_naming_of lthy) (Local_Theory.operations_of lthy) after_close
end;
in
@@ -137,4 +138,3 @@
end |> Pretty.writeln_chunks;
end;
-
--- a/src/Pure/Isar/class.ML Wed Apr 01 19:17:41 2015 +0200
+++ b/src/Pure/Isar/class.ML Wed Apr 01 22:40:41 2015 +0200
@@ -599,8 +599,6 @@
fun instantiation (tycos, vs, sort) thy =
let
- val naming = Sign.naming_of thy;
-
val _ = if null tycos then error "At least one arity must be given" else ();
val class_params = these_params thy (filter (can (Axclass.get_info thy)) sort);
fun get_param tyco (param, (_, (c, ty))) =
@@ -637,7 +635,7 @@
|> Overloading.activate_improvable_syntax
|> Context.proof_map (Syntax_Phases.term_check 0 "resorting" resort_check)
|> synchronize_inst_syntax
- |> Local_Theory.init naming
+ |> Local_Theory.init (Sign.naming_of thy)
{define = Generic_Target.define foundation,
notes = Generic_Target.notes Generic_Target.theory_notes,
abbrev = Generic_Target.abbrev Generic_Target.theory_abbrev,
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Isar/experiment.ML Wed Apr 01 22:40:41 2015 +0200
@@ -0,0 +1,29 @@
+(* Title: Pure/Isar/experiment.ML
+ Author: Makarius
+
+Target for specification experiments that are mostly private.
+*)
+
+signature EXPERIMENT =
+sig
+ val experiment: Element.context_i list -> theory -> Binding.scope * local_theory
+ val experiment_cmd: Element.context list -> theory -> Binding.scope * local_theory
+end;
+
+structure Experiment: EXPERIMENT =
+struct
+
+fun gen_experiment add_locale elems thy =
+ let
+ val (_, lthy) = thy
+ |> add_locale (Binding.name ("experiment" ^ serial_string ())) Binding.empty ([], []) elems;
+ val (scope, naming) =
+ Name_Space.new_scope (Proof_Context.naming_of (Local_Theory.target_of lthy));
+ val naming' = naming |> Name_Space.private scope;
+ val lthy' = lthy |> Local_Theory.map_contexts (K (Proof_Context.map_naming (K naming')));
+ in (scope, lthy') end;
+
+val experiment = gen_experiment Expression.add_locale;
+val experiment_cmd = gen_experiment Expression.add_locale_cmd;
+
+end;
--- a/src/Pure/Isar/isar_syn.ML Wed Apr 01 19:17:41 2015 +0200
+++ b/src/Pure/Isar/isar_syn.ML Wed Apr 01 22:40:41 2015 +0200
@@ -361,7 +361,7 @@
((Parse.position Parse.xname >> (fn name =>
Toplevel.begin_local_theory true (Named_Target.begin name)) ||
Scan.optional Parse_Spec.includes [] -- Scan.repeat Parse_Spec.context_element
- >> (fn (incls, elems) => Toplevel.open_target (Bundle.context_cmd incls elems)))
+ >> (fn (incls, elems) => Toplevel.open_target (#2 o Bundle.context_cmd incls elems)))
--| Parse.begin);
@@ -373,13 +373,19 @@
Scan.repeat1 Parse_Spec.context_element >> pair ([], []);
val _ =
- Outer_Syntax.command @{command_spec "locale"} "define named proof context"
+ Outer_Syntax.command @{command_spec "locale"} "define named specification context"
(Parse.binding --
Scan.optional (@{keyword "="} |-- Parse.!!! locale_val) (([], []), []) -- Parse.opt_begin
>> (fn ((name, (expr, elems)), begin) =>
Toplevel.begin_local_theory begin
(Expression.add_locale_cmd name Binding.empty expr elems #> snd)));
+val _ =
+ Outer_Syntax.command @{command_spec "experiment"} "open private specification context"
+ (Scan.repeat Parse_Spec.context_element --| Parse.begin
+ >> (fn elems =>
+ Toplevel.begin_local_theory true (Experiment.experiment_cmd elems #> snd)));
+
fun interpretation_args mandatory =
Parse.!!! (Parse_Spec.locale_expression mandatory) --
Scan.optional
--- a/src/Pure/Isar/local_theory.ML Wed Apr 01 19:17:41 2015 +0200
+++ b/src/Pure/Isar/local_theory.ML Wed Apr 01 22:40:41 2015 +0200
@@ -21,17 +21,14 @@
val assert_bottom: bool -> local_theory -> local_theory
val mark_brittle: local_theory -> local_theory
val assert_nonbrittle: local_theory -> local_theory
- val open_target: Name_Space.naming -> operations -> (local_theory -> local_theory) ->
+ val map_contexts: (int -> Proof.context -> Proof.context) -> local_theory -> local_theory
+ val background_naming_of: local_theory -> Name_Space.naming
+ val map_background_naming: (Name_Space.naming -> Name_Space.naming) ->
local_theory -> local_theory
- val close_target: local_theory -> local_theory
- val map_contexts: (int -> Proof.context -> Proof.context) -> local_theory -> local_theory
- val naming_of: local_theory -> Name_Space.naming
+ val restore_background_naming: local_theory -> local_theory -> local_theory
val full_name: local_theory -> binding -> string
- val map_naming: (Name_Space.naming -> Name_Space.naming) -> local_theory -> local_theory
- val concealed: local_theory -> local_theory
val new_group: local_theory -> local_theory
val reset_group: local_theory -> local_theory
- val restore_naming: local_theory -> local_theory -> local_theory
val standard_morphism: local_theory -> Proof.context -> morphism
val standard_form: local_theory -> Proof.context -> (morphism -> 'a) -> 'a
val raw_theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
@@ -73,6 +70,10 @@
val exit_global: local_theory -> theory
val exit_result: (morphism -> 'a -> 'b) -> 'a * local_theory -> 'b * Proof.context
val exit_result_global: (morphism -> 'a -> 'b) -> 'a * local_theory -> 'b * theory
+ val init_target: Name_Space.naming -> operations -> (local_theory -> local_theory) ->
+ local_theory -> Binding.scope * local_theory
+ val open_target: local_theory -> Binding.scope * local_theory
+ val close_target: local_theory -> local_theory
end;
structure Local_Theory: LOCAL_THEORY =
@@ -97,15 +98,15 @@
exit: local_theory -> Proof.context};
type lthy =
- {naming: Name_Space.naming,
+ {background_naming: Name_Space.naming,
operations: operations,
after_close: local_theory -> local_theory,
brittle: bool,
target: Proof.context};
-fun make_lthy (naming, operations, after_close, brittle, target) : lthy =
- {naming = naming, operations = operations, after_close = after_close,
- brittle = brittle, target = target};
+fun make_lthy (background_naming, operations, after_close, brittle, target) : lthy =
+ {background_naming = background_naming, operations = operations,
+ after_close = after_close, brittle = brittle, target = target};
(* context data *)
@@ -124,8 +125,8 @@
fun map_top f =
assert #>
- Data.map (fn {naming, operations, after_close, brittle, target} :: parents =>
- make_lthy (f (naming, operations, after_close, brittle, target)) :: parents);
+ Data.map (fn {background_naming, operations, after_close, brittle, target} :: parents =>
+ make_lthy (f (background_naming, operations, after_close, brittle, target)) :: parents);
fun restore lthy = #target (top_of lthy) |> Data.put (Data.get lthy);
@@ -144,25 +145,16 @@
else lthy
end;
-fun open_target naming operations after_close target =
- assert target
- |> Data.map (cons (make_lthy (naming, operations, after_close, true, target)));
-
-fun close_target lthy =
- let
- val _ = assert_bottom false lthy;
- val ({after_close, ...} :: rest) = Data.get lthy;
- in lthy |> Data.put rest |> restore |> after_close end;
-
fun map_contexts f lthy =
let val n = level lthy in
- lthy |> (Data.map o map_index) (fn (i, {naming, operations, after_close, brittle, target}) =>
- make_lthy (naming, operations, after_close, brittle,
- target
- |> Context_Position.set_visible false
- |> f (n - i - 1)
- |> Context_Position.restore_visible target))
- |> f n
+ lthy |> (Data.map o map_index)
+ (fn (i, {background_naming, operations, after_close, brittle, target}) =>
+ make_lthy (background_naming, operations, after_close, brittle,
+ target
+ |> Context_Position.set_visible false
+ |> f (n - i - 1)
+ |> Context_Position.restore_visible target))
+ |> f n
end;
@@ -170,8 +162,8 @@
fun mark_brittle lthy =
if level lthy = 1 then
- map_top (fn (naming, operations, after_close, _, target) =>
- (naming, operations, after_close, true, target)) lthy
+ map_top (fn (background_naming, operations, after_close, _, target) =>
+ (background_naming, operations, after_close, true, target)) lthy
else lthy;
fun assert_nonbrittle lthy =
@@ -179,20 +171,20 @@
else lthy;
-(* naming *)
+(* naming for background theory *)
-val naming_of = #naming o top_of;
-val full_name = Name_Space.full_name o naming_of;
+val background_naming_of = #background_naming o top_of;
-fun map_naming f =
- map_top (fn (naming, operations, after_close, brittle, target) =>
- (f naming, operations, after_close, brittle, target));
+fun map_background_naming f =
+ map_top (fn (background_naming, operations, after_close, brittle, target) =>
+ (f background_naming, operations, after_close, brittle, target));
-val concealed = map_naming Name_Space.concealed;
-val new_group = map_naming Name_Space.new_group;
-val reset_group = map_naming Name_Space.reset_group;
+val restore_background_naming = map_background_naming o K o background_naming_of;
-val restore_naming = map_naming o K o naming_of;
+val full_name = Name_Space.full_name o background_naming_of;
+
+val new_group = map_background_naming Name_Space.new_group;
+val reset_group = map_background_naming Name_Space.reset_group;
(* standard morphisms *)
@@ -200,7 +192,7 @@
fun standard_morphism lthy ctxt =
Proof_Context.norm_export_morphism lthy ctxt $>
Morphism.binding_morphism "Local_Theory.standard_binding"
- (Name_Space.transform_binding (naming_of lthy));
+ (Name_Space.transform_binding (Proof_Context.naming_of lthy));
fun standard_form lthy ctxt x =
Morphism.form (Morphism.transform (standard_morphism lthy ctxt) x);
@@ -217,11 +209,17 @@
fun raw_theory f = #2 o raw_theory_result (f #> pair ());
fun background_theory_result f lthy =
- lthy |> raw_theory_result (fn thy =>
- thy
- |> Sign.map_naming (K (naming_of lthy))
- |> f
- ||> Sign.restore_naming thy);
+ let
+ val naming =
+ background_naming_of lthy
+ |> Name_Space.transform_naming (Proof_Context.naming_of lthy);
+ in
+ lthy |> raw_theory_result (fn thy =>
+ thy
+ |> Sign.map_naming (K naming)
+ |> f
+ ||> Sign.restore_naming thy)
+ end;
fun background_theory f = #2 o background_theory_result (f #> pair ());
@@ -339,18 +337,15 @@
-(** init and exit **)
+(** manage targets **)
-(* init *)
+(* outermost target *)
-fun init naming operations target =
+fun init background_naming operations target =
target |> Data.map
- (fn [] => [make_lthy (naming, operations, I, false, target)]
+ (fn [] => [make_lthy (background_naming, operations, I, false, target)]
| _ => error "Local theory already initialized");
-
-(* exit *)
-
val exit = operation #exit;
val exit_global = Proof_Context.theory_of o exit;
@@ -367,4 +362,25 @@
val phi = standard_morphism lthy thy_ctxt;
in (f phi x, thy) end;
+
+(* nested targets *)
+
+fun init_target background_naming operations after_close lthy =
+ let
+ val _ = assert lthy;
+ val (scope, target) = Proof_Context.new_scope lthy;
+ val lthy' =
+ target
+ |> Data.map (cons (make_lthy (background_naming, operations, after_close, true, target)));
+ in (scope, lthy') end;
+
+fun open_target lthy =
+ init_target (background_naming_of lthy) (operations_of lthy) I lthy;
+
+fun close_target lthy =
+ let
+ val _ = assert_bottom false lthy;
+ val ({after_close, ...} :: rest) = Data.get lthy;
+ in lthy |> Data.put rest |> restore |> after_close end;
+
end;
--- a/src/Pure/Isar/locale.ML Wed Apr 01 19:17:41 2015 +0200
+++ b/src/Pure/Isar/locale.ML Wed Apr 01 22:40:41 2015 +0200
@@ -180,7 +180,7 @@
fun markup_name ctxt name = markup_extern ctxt name |-> Markup.markup;
fun pretty_name ctxt name = markup_extern ctxt name |> Pretty.mark_str;
-val get_locale = Option.map #2 oo (Name_Space.lookup_key o Locales.get);
+val get_locale = Name_Space.lookup o Locales.get;
val defined = is_some oo get_locale;
fun the_locale thy name =
--- a/src/Pure/Isar/named_target.ML Wed Apr 01 19:17:41 2015 +0200
+++ b/src/Pure/Isar/named_target.ML Wed Apr 01 22:40:41 2015 +0200
@@ -155,14 +155,14 @@
fun gen_init before_exit target thy =
let
val name_data = make_name_data thy target;
- val naming = Sign.naming_of thy
- |> Name_Space.mandatory_path (Long_Name.base_name target);
+ val background_naming =
+ Sign.naming_of thy |> Name_Space.mandatory_path (Long_Name.base_name target);
in
thy
|> Sign.change_begin
|> init_context name_data
|> is_none before_exit ? Data.put (SOME name_data)
- |> Local_Theory.init naming
+ |> Local_Theory.init background_naming
{define = Generic_Target.define (foundation name_data),
notes = Generic_Target.notes (notes name_data),
abbrev = Generic_Target.abbrev (abbrev name_data),
--- a/src/Pure/Isar/overloading.ML Wed Apr 01 19:17:41 2015 +0200
+++ b/src/Pure/Isar/overloading.ML Wed Apr 01 22:40:41 2015 +0200
@@ -189,7 +189,6 @@
fun gen_overloading prep_const raw_overloading thy =
let
val ctxt = Proof_Context.init_global thy;
- val naming = Sign.naming_of thy;
val _ = if null raw_overloading then error "At least one parameter must be given" else ();
val overloading = raw_overloading |> map (fn (v, const, checked) =>
(Term.dest_Const (prep_const ctxt const), (v, checked)));
@@ -201,7 +200,7 @@
|> fold (fn ((_, ty), (v, _)) => Variable.declare_names (Free (v, ty))) overloading
|> activate_improvable_syntax
|> synchronize_syntax
- |> Local_Theory.init naming
+ |> Local_Theory.init (Sign.naming_of thy)
{define = Generic_Target.define foundation,
notes = Generic_Target.notes Generic_Target.theory_notes,
abbrev = Generic_Target.abbrev Generic_Target.theory_abbrev,
--- a/src/Pure/Isar/proof_context.ML Wed Apr 01 19:17:41 2015 +0200
+++ b/src/Pure/Isar/proof_context.ML Wed Apr 01 22:40:41 2015 +0200
@@ -34,6 +34,10 @@
val naming_of: Proof.context -> Name_Space.naming
val restore_naming: Proof.context -> Proof.context -> Proof.context
val full_name: Proof.context -> binding -> string
+ val get_scope: Proof.context -> Binding.scope option
+ val new_scope: Proof.context -> Binding.scope * Proof.context
+ val private: Binding.scope -> Proof.context -> Proof.context
+ val concealed: Proof.context -> Proof.context
val class_space: Proof.context -> Name_Space.T
val type_space: Proof.context -> Name_Space.T
val const_space: Proof.context -> Name_Space.T
@@ -304,6 +308,17 @@
val full_name = Name_Space.full_name o naming_of;
+val get_scope = Name_Space.get_scope o naming_of;
+
+fun new_scope ctxt =
+ let
+ val (scope, naming') = Name_Space.new_scope (naming_of ctxt);
+ val ctxt' = map_naming (K naming') ctxt;
+ in (scope, ctxt') end;
+
+val private = map_naming o Name_Space.private;
+val concealed = map_naming Name_Space.concealed;
+
(* name spaces *)
--- a/src/Pure/ML/ml_antiquotations.ML Wed Apr 01 19:17:41 2015 +0200
+++ b/src/Pure/ML/ml_antiquotations.ML Wed Apr 01 22:40:41 2015 +0200
@@ -47,7 +47,7 @@
|> filter completed
|> map (fn a => (a, ("system_option", a))));
val report = Markup.markup_report (Completion.reported_text completion);
- in cat_error msg report end;
+ in error (msg ^ report) end;
val _ = Context_Position.report ctxt pos markup;
in ML_Syntax.print_string name end)) #>
--- a/src/Pure/PIDE/batch_session.scala Wed Apr 01 19:17:41 2015 +0200
+++ b/src/Pure/PIDE/batch_session.scala Wed Apr 01 22:40:41 2015 +0200
@@ -19,7 +19,7 @@
session: String): Batch_Session =
{
val (_, session_tree) =
- Build.find_sessions(options, dirs).selection(false, false, Nil, List(session))
+ Build.find_sessions(options, dirs).selection(sessions = List(session))
val session_info = session_tree(session)
val parent_session =
session_info.parent getOrElse error("No parent session for " + quote(session))
@@ -29,7 +29,7 @@
dirs = dirs, sessions = List(parent_session)) != 0)
new RuntimeException
- val deps = Build.dependencies(Build.Ignore_Progress, false, verbose, false, session_tree)
+ val deps = Build.dependencies(verbose = verbose, tree = session_tree)
val resources =
{
val content = deps(parent_session)
--- a/src/Pure/Pure.thy Wed Apr 01 19:17:41 2015 +0200
+++ b/src/Pure/Pure.thy Wed Apr 01 22:40:41 2015 +0200
@@ -33,7 +33,7 @@
and "bundle" :: thy_decl
and "include" "including" :: prf_decl
and "print_bundles" :: diag
- and "context" "locale" :: thy_decl_block
+ and "context" "locale" "experiment" :: thy_decl_block
and "sublocale" "interpretation" :: thy_goal
and "interpret" :: prf_goal % "proof"
and "class" :: thy_decl_block
--- a/src/Pure/ROOT Wed Apr 01 19:17:41 2015 +0200
+++ b/src/Pure/ROOT Wed Apr 01 22:40:41 2015 +0200
@@ -121,6 +121,7 @@
"Isar/code.ML"
"Isar/context_rules.ML"
"Isar/element.ML"
+ "Isar/experiment.ML"
"Isar/expression.ML"
"Isar/generic_target.ML"
"Isar/isar_cmd.ML"
--- a/src/Pure/ROOT.ML Wed Apr 01 19:17:41 2015 +0200
+++ b/src/Pure/ROOT.ML Wed Apr 01 22:40:41 2015 +0200
@@ -273,6 +273,7 @@
use "Isar/expression.ML";
use "Isar/class_declaration.ML";
use "Isar/bundle.ML";
+use "Isar/experiment.ML";
use "simplifier.ML";
use "Tools/plugin.ML";
--- a/src/Pure/Tools/build.scala Wed Apr 01 19:17:41 2015 +0200
+++ b/src/Pure/Tools/build.scala Wed Apr 01 22:40:41 2015 +0200
@@ -162,12 +162,18 @@
def apply(name: String): Session_Info = graph.get_node(name)
def isDefinedAt(name: String): Boolean = graph.defined(name)
- def selection(requirements: Boolean, all_sessions: Boolean,
- session_groups: List[String], sessions: List[String]): (List[String], Session_Tree) =
+ def selection(
+ requirements: Boolean = false,
+ all_sessions: Boolean = false,
+ session_groups: List[String] = Nil,
+ exclude_sessions: List[String] = Nil,
+ sessions: List[String] = Nil): (List[String], Session_Tree) =
{
- val bad_sessions = sessions.filterNot(isDefinedAt(_))
+ val bad_sessions =
+ SortedSet((exclude_sessions ::: sessions).filterNot(isDefinedAt(_)): _*).toList
if (bad_sessions.nonEmpty) error("Undefined session(s): " + commas_quote(bad_sessions))
+ val excluded = graph.all_succs(exclude_sessions).toSet
val pre_selected =
{
if (all_sessions) graph.keys
@@ -179,7 +185,8 @@
if info.select || select(name) || apply(name).groups.exists(select_group)
} yield name).toList
}
- }
+ }.filterNot(excluded)
+
val selected =
if (requirements) (graph.all_preds(pre_selected).toSet -- pre_selected).toList
else pre_selected
@@ -427,8 +434,13 @@
def sources(name: String): List[SHA1.Digest] = deps(name).sources.map(_._2)
}
- def dependencies(progress: Progress, inlined_files: Boolean,
- verbose: Boolean, list_files: Boolean, tree: Session_Tree): Deps =
+ def dependencies(
+ progress: Progress = Ignore_Progress,
+ inlined_files: Boolean = false,
+ verbose: Boolean = false,
+ list_files: Boolean = false,
+ check_keywords: Set[String] = Set.empty,
+ tree: Session_Tree): Deps =
Deps((Map.empty[String, Session_Content] /: tree.topological_order)(
{ case (deps, (name, info)) =>
if (progress.stopped) throw Exn.Interrupt()
@@ -484,16 +496,20 @@
val keywords = thy_deps.keywords
val syntax = thy_deps.syntax.asInstanceOf[Outer_Syntax]
+ val theory_files = thy_deps.deps.map(dep => Path.explode(dep.name.node))
val loaded_files = if (inlined_files) thy_deps.loaded_files else Nil
val all_files =
- (thy_deps.deps.map(dep => Path.explode(dep.name.node)) ::: loaded_files :::
+ (theory_files ::: loaded_files :::
info.files.map(file => info.dir + file) :::
info.document_files.map(file => info.dir + file._1 + file._2)).map(_.expand)
if (list_files)
progress.echo(cat_lines(all_files.map(_.implode).sorted.map(" " + _)))
+ if (check_keywords.nonEmpty)
+ Check_Keywords.check_keywords(progress, syntax.keywords, check_keywords, theory_files)
+
val sources = all_files.map(p => (p, SHA1.digest(p.file)))
val session_graph = thy_deps.deps_graph(info.parent getOrElse "", loaded_theories0)
@@ -516,8 +532,8 @@
dirs: List[Path],
sessions: List[String]): Deps =
{
- val (_, tree) = find_sessions(options, dirs = dirs).selection(false, false, Nil, sessions)
- dependencies(Ignore_Progress, inlined_files, false, false, tree)
+ val (_, tree) = find_sessions(options, dirs = dirs).selection(sessions = sessions)
+ dependencies(inlined_files = inlined_files, tree = tree)
}
def session_content(
@@ -737,18 +753,20 @@
session_groups: List[String] = Nil,
max_jobs: Int = 1,
list_files: Boolean = false,
+ check_keywords: Set[String] = Set.empty,
no_build: Boolean = false,
system_mode: Boolean = false,
verbose: Boolean = false,
+ exclude_sessions: List[String] = Nil,
sessions: List[String] = Nil): Map[String, Int] =
{
/* session tree and dependencies */
val full_tree = find_sessions(options.int("completion_limit") = 0, dirs, select_dirs)
val (selected, selected_tree) =
- full_tree.selection(requirements, all_sessions, session_groups, sessions)
+ full_tree.selection(requirements, all_sessions, session_groups, exclude_sessions, sessions)
- val deps = dependencies(progress, true, verbose, list_files, selected_tree)
+ val deps = dependencies(progress, true, verbose, list_files, check_keywords, selected_tree)
def make_stamp(name: String): String =
sources_stamp(selected_tree(name).entry_digest :: deps.sources(name))
@@ -988,15 +1006,17 @@
session_groups: List[String] = Nil,
max_jobs: Int = 1,
list_files: Boolean = false,
+ check_keywords: Set[String] = Set.empty,
no_build: Boolean = false,
system_mode: Boolean = false,
verbose: Boolean = false,
+ exclude_sessions: List[String] = Nil,
sessions: List[String] = Nil): Int =
{
val results =
- build_results(options, progress, requirements, all_sessions,
- build_heap, clean_build, dirs, select_dirs, session_groups, max_jobs,
- list_files, no_build, system_mode, verbose, sessions)
+ build_results(options, progress, requirements, all_sessions, build_heap, clean_build,
+ dirs, select_dirs, session_groups, max_jobs, list_files, check_keywords,
+ no_build, system_mode, verbose, exclude_sessions, sessions)
val rc = (0 /: results)({ case (rc1, (_, rc2)) => rc1 max rc2 })
if (rc != 0 && (verbose || !no_build)) {
@@ -1024,13 +1044,15 @@
Properties.Value.Boolean(no_build) ::
Properties.Value.Boolean(system_mode) ::
Properties.Value.Boolean(verbose) ::
- Command_Line.Chunks(dirs, select_dirs, session_groups, build_options, sessions) =>
+ Command_Line.Chunks(dirs, select_dirs, session_groups, check_keywords,
+ build_options, exclude_sessions, sessions) =>
val options = (Options.init() /: build_options)(_ + _)
val progress = new Console_Progress(verbose)
progress.interrupt_handler {
build(options, progress, requirements, all_sessions, build_heap, clean_build,
dirs.map(Path.explode(_)), select_dirs.map(Path.explode(_)), session_groups,
- max_jobs, list_files, no_build, system_mode, verbose, sessions)
+ max_jobs, list_files, check_keywords.toSet, no_build, system_mode,
+ verbose, exclude_sessions, sessions)
}
case _ => error("Bad arguments:\n" + cat_lines(args))
}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/check_keywords.scala Wed Apr 01 22:40:41 2015 +0200
@@ -0,0 +1,54 @@
+/* Title: Pure/Tools/check_keywords.scala
+ Author: Makarius
+
+Check theory sources for conflicts with proposed keywords.
+*/
+
+package isabelle
+
+
+object Check_Keywords
+{
+ def conflicts(
+ keywords: Keyword.Keywords,
+ check: Set[String],
+ input: CharSequence,
+ start: Token.Pos): List[(Token, Position.T)] =
+ {
+ object Parser extends Parse.Parser
+ {
+ private val conflict =
+ position(token("token", tok => !(tok.is_command || tok.is_keyword) && check(tok.source)))
+ private val other = token("token", _ => true)
+ private val item = conflict ^^ (x => Some(x)) | other ^^ (_ => None)
+
+ val result =
+ parse_all(rep(item), Token.reader(Token.explode(keywords, input), start)) match {
+ case Success(res, _) => for (Some(x) <- res) yield x
+ case bad => error(bad.toString)
+ }
+ }
+ Parser.result
+ }
+
+ def check_keywords(
+ progress: Build.Progress,
+ keywords: Keyword.Keywords,
+ check: Set[String],
+ paths: List[Path])
+ {
+ val parallel_args = paths.map(path => (File.read(path), Token.Pos.file(path.expand.implode)))
+
+ val bad =
+ Par_List.map((arg: (String, Token.Pos)) => {
+ if (progress.stopped) throw Exn.Interrupt()
+ conflicts(keywords, check, arg._1, arg._2)
+ }, parallel_args).flatten
+
+ for ((tok, pos) <- bad) {
+ progress.echo(Output.warning_text(
+ "keyword conflict: " + tok.kind.toString + " " + quote(tok.content) +
+ Position.here(pos)))
+ }
+ }
+}
--- a/src/Pure/Tools/find_theorems.ML Wed Apr 01 19:17:41 2015 +0200
+++ b/src/Pure/Tools/find_theorems.ML Wed Apr 01 22:40:41 2015 +0200
@@ -328,7 +328,7 @@
local
val index_ord = option_ord (K EQUAL);
-val hidden_ord = bool_ord o apply2 Long_Name.is_hidden;
+val hidden_ord = bool_ord o apply2 (is_some o Long_Name.dest_hidden);
val qual_ord = int_ord o apply2 Long_Name.qualification;
val txt_ord = int_ord o apply2 size;
--- a/src/Pure/Tools/named_theorems.ML Wed Apr 01 19:17:41 2015 +0200
+++ b/src/Pure/Tools/named_theorems.ML Wed Apr 01 22:40:41 2015 +0200
@@ -61,7 +61,7 @@
fun declare binding descr lthy =
let
- val name = Name_Space.full_name (Local_Theory.naming_of lthy) binding;
+ val name = Local_Theory.full_name lthy binding;
val description =
"declaration of " ^ (if descr = "" then Binding.name_of binding ^ " rules" else descr);
val lthy' = lthy
@@ -86,7 +86,7 @@
let
val thy = Proof_Context.theory_of ctxt;
val name = Global_Theory.check_fact thy (xname, pos);
- val _ = get ctxt name handle ERROR msg => cat_error msg (Position.here pos);
+ val _ = get ctxt name handle ERROR msg => error (msg ^ Position.here pos);
in ML_Syntax.print_string name end)));
end;
--- a/src/Pure/Tools/plugin.ML Wed Apr 01 19:17:41 2015 +0200
+++ b/src/Pure/Tools/plugin.ML Wed Apr 01 22:40:41 2015 +0200
@@ -138,9 +138,9 @@
fun apply change_naming (interp: interp) (data: data) lthy =
lthy
- |> change_naming ? Local_Theory.map_naming (K (#naming data))
+ |> change_naming ? Local_Theory.map_background_naming (K (#naming data))
|> #apply interp (#value data)
- |> Local_Theory.restore_naming lthy;
+ |> Local_Theory.restore_background_naming lthy;
fun unfinished data (interp: interp, data') =
(interp,
--- a/src/Pure/build-jars Wed Apr 01 19:17:41 2015 +0200
+++ b/src/Pure/build-jars Wed Apr 01 22:40:41 2015 +0200
@@ -92,6 +92,7 @@
Tools/build.scala
Tools/build_console.scala
Tools/build_doc.scala
+ Tools/check_keywords.scala
Tools/check_source.scala
Tools/doc.scala
Tools/main.scala
--- a/src/Pure/facts.ML Wed Apr 01 19:17:41 2015 +0200
+++ b/src/Pure/facts.ML Wed Apr 01 22:40:41 2015 +0200
@@ -166,13 +166,13 @@
(* retrieve *)
-val defined = is_some oo (Name_Space.lookup_key o facts_of);
+val defined = Name_Space.defined o facts_of;
fun lookup context facts name =
- (case Name_Space.lookup_key (facts_of facts) name of
+ (case Name_Space.lookup (facts_of facts) name of
NONE => NONE
- | SOME (_, Static ths) => SOME (true, ths)
- | SOME (_, Dynamic f) => SOME (false, f context));
+ | SOME (Static ths) => SOME (true, ths)
+ | SOME (Dynamic f) => SOME (false, f context));
fun retrieve context facts (xname, pos) =
let
--- a/src/Pure/sign.ML Wed Apr 01 19:17:41 2015 +0200
+++ b/src/Pure/sign.ML Wed Apr 01 22:40:41 2015 +0200
@@ -101,6 +101,8 @@
(string * (Proof.context -> Ast.ast list -> Ast.ast)) list -> theory -> theory
val add_trrules: Ast.ast Syntax.trrule list -> theory -> theory
val del_trrules: Ast.ast Syntax.trrule list -> theory -> theory
+ val get_scope: theory -> Binding.scope option
+ val new_scope: theory -> Binding.scope * theory
val new_group: theory -> theory
val reset_group: theory -> theory
val add_path: string -> theory -> theory
@@ -109,6 +111,8 @@
val mandatory_path: string -> theory -> theory
val qualified_path: bool -> binding -> theory -> theory
val local_path: theory -> theory
+ val private: Binding.scope -> theory -> theory
+ val concealed: theory -> theory
val hide_class: bool -> string -> theory -> theory
val hide_type: bool -> string -> theory -> theory
val hide_const: bool -> string -> theory -> theory
@@ -499,6 +503,14 @@
(* naming *)
+val get_scope = Name_Space.get_scope o naming_of;
+
+fun new_scope thy =
+ let
+ val (scope, naming') = Name_Space.new_scope (naming_of thy);
+ val thy' = map_naming (K naming') thy;
+ in (scope, thy') end;
+
val new_group = map_naming Name_Space.new_group;
val reset_group = map_naming Name_Space.reset_group;
@@ -510,6 +522,9 @@
fun local_path thy = thy |> root_path |> add_path (Context.theory_name thy);
+val private = map_naming o Name_Space.private;
+val concealed = map_naming Name_Space.concealed;
+
(* hide names *)
--- a/src/Pure/thm.ML Wed Apr 01 19:17:41 2015 +0200
+++ b/src/Pure/thm.ML Wed Apr 01 22:40:41 2015 +0200
@@ -590,8 +590,8 @@
fun axiom theory name =
let
fun get_ax thy =
- Name_Space.lookup_key (Theory.axiom_table thy) name
- |> Option.map (fn (_, prop) =>
+ Name_Space.lookup (Theory.axiom_table thy) name
+ |> Option.map (fn prop =>
let
val der = deriv_rule0 (Proofterm.axm_proof name prop);
val maxidx = maxidx_of_term prop;
--- a/src/Pure/type.ML Wed Apr 01 19:17:41 2015 +0200
+++ b/src/Pure/type.ML Wed Apr 01 22:40:41 2015 +0200
@@ -254,7 +254,7 @@
fun undecl_type c = "Undeclared type constructor: " ^ quote c;
-fun lookup_type (TSig {types, ...}) = Option.map #2 o Name_Space.lookup_key types;
+fun lookup_type (TSig {types, ...}) = Name_Space.lookup types;
fun check_decl context (TSig {types, ...}) (c, pos) =
Name_Space.check_reports context types (c, [pos]);
@@ -659,8 +659,9 @@
let
val types' = f types;
val _ =
+ not (Name_Space.defined types' "dummy") orelse
Name_Space.intern (Name_Space.space_of_table types') "dummy" = "dummy" orelse
- error "Illegal declaration of dummy type";
+ error "Illegal declaration of dummy type";
in (classes, default, types') end);
fun syntactic tsig (Type (c, Ts)) =
--- a/src/Pure/variable.ML Wed Apr 01 19:17:41 2015 +0200
+++ b/src/Pure/variable.ML Wed Apr 01 22:40:41 2015 +0200
@@ -340,14 +340,14 @@
fun restore_proper_fixes ctxt = Config.put proper_fixes (Config.get ctxt proper_fixes);
fun is_improper ctxt x =
- (case Name_Space.lookup_key (fixes_of ctxt) x of
- SOME (_, (_, proper)) => not proper
+ (case Name_Space.lookup (fixes_of ctxt) x of
+ SOME (_, proper) => not proper
| NONE => false);
(* specialized name space *)
-val is_fixed = Name_Space.defined_entry o fixes_space;
+val is_fixed = Name_Space.defined o fixes_of;
fun is_newly_fixed inner outer = is_fixed inner andf (not o is_fixed outer);
val fixed_ord = Name_Space.entry_ord o fixes_space;
@@ -358,8 +358,8 @@
in if is_fixed ctxt x' then SOME x' else NONE end;
fun revert_fixed ctxt x =
- (case Name_Space.lookup_key (fixes_of ctxt) x of
- SOME (_, (x', _)) => if intern_fixed ctxt x' = x then x' else x
+ (case Name_Space.lookup (fixes_of ctxt) x of
+ SOME (x', _) => if intern_fixed ctxt x' = x then x' else x
| NONE => x);
fun markup_fixed ctxt x =