--- a/src/Pure/General/name_space.ML Thu Oct 11 14:38:58 2012 +0200
+++ b/src/Pure/General/name_space.ML Thu Oct 11 21:02:19 2012 +0200
@@ -90,12 +90,12 @@
fun entry_markup def kind (name, {pos, id, ...}: entry) =
Markup.properties (Position.entity_properties_of def id pos) (Isabelle_Markup.entity kind name);
-fun print_entry def kind (name, entry) =
- quote (Markup.markup (entry_markup def kind (name, entry)) name);
+fun print_entry_ref kind (name, entry) =
+ quote (Markup.markup (entry_markup false kind (name, entry)) name);
-fun err_dup kind entry1 entry2 =
+fun err_dup kind entry1 entry2 pos =
error ("Duplicate " ^ kind ^ " declaration " ^
- print_entry true kind entry1 ^ " vs. " ^ print_entry true kind entry2);
+ print_entry_ref kind entry1 ^ " vs. " ^ print_entry_ref kind entry2 ^ Position.here pos);
fun undefined kind name = "Undefined " ^ kind ^ ": " ^ quote name;
@@ -239,7 +239,7 @@
val entries' = (entries1, entries2) |> Symtab.join
(fn name => fn ((_, entry1), (_, entry2)) =>
if #id entry1 = #id entry2 then raise Symtab.SAME
- else err_dup kind' (name, entry1) (name, entry2));
+ else err_dup kind' (name, entry1) (name, entry2) Position.none);
in make_name_space (kind', internals', entries') end;
@@ -387,7 +387,7 @@
val entries' =
(if strict then Symtab.update_new else Symtab.update) (name, (externals, entry)) entries
handle Symtab.DUP dup =>
- err_dup kind (dup, #2 (the (Symtab.lookup entries dup))) (name, entry);
+ err_dup kind (dup, #2 (the (Symtab.lookup entries dup))) (name, entry) (#pos entry);
in (kind, internals, entries') end);
fun declare context strict binding space =
--- a/src/Pure/Isar/expression.ML Thu Oct 11 14:38:58 2012 +0200
+++ b/src/Pure/Isar/expression.ML Thu Oct 11 21:02:19 2012 +0200
@@ -144,13 +144,14 @@
local
fun prep_inst prep_term ctxt parms (Positional insts) =
- (insts ~~ parms) |> map (fn
- (NONE, p) => Free (p, dummyT) |
- (SOME t, _) => prep_term ctxt t)
+ (insts ~~ parms) |> map
+ (fn (NONE, p) => Free (p, dummyT)
+ | (SOME t, _) => prep_term ctxt t)
| prep_inst prep_term ctxt parms (Named insts) =
- parms |> map (fn p => case AList.lookup (op =) insts p of
- SOME t => prep_term ctxt t |
- NONE => Free (p, dummyT));
+ parms |> map (fn p =>
+ (case AList.lookup (op =) insts p of
+ SOME t => prep_term ctxt t |
+ NONE => Free (p, dummyT)));
in
@@ -286,15 +287,29 @@
(** Finish locale elements **)
+fun finish_inst ctxt (loc, (prfx, inst)) =
+ let
+ val thy = Proof_Context.theory_of ctxt;
+ val (parm_names, parm_types) = Locale.params_of thy loc |> map #1 |> split_list;
+ val (morph, _) = inst_morph (parm_names, parm_types) (prfx, inst) ctxt;
+ in (loc, morph) end;
+
+fun finish_fixes (parms: (string * typ) list) = map (fn (binding, _, mx) =>
+ let val x = Binding.name_of binding
+ in (binding, AList.lookup (op =) parms x, mx) end);
+
+local
+
fun closeup _ _ false elem = elem
- | closeup ctxt parms true elem =
+ | closeup (outer_ctxt, ctxt) parms true elem =
let
(* FIXME consider closing in syntactic phase -- before type checking *)
fun close_frees t =
let
val rev_frees =
Term.fold_aterms (fn Free (x, T) =>
- if AList.defined (op =) parms x then I else insert (op =) (x, T) | _ => I) t [];
+ if Variable.is_fixed outer_ctxt x orelse AList.defined (op =) parms x then I
+ else insert (op =) (x, T) | _ => I) t [];
in fold (Logic.all o Free) rev_frees t end;
fun no_binds [] = []
@@ -309,29 +324,15 @@
| e => e)
end;
-fun finish_primitive parms _ (Fixes fixes) = Fixes (map (fn (binding, _, mx) =>
- let val x = Binding.name_of binding
- in (binding, AList.lookup (op =) parms x, mx) end) fixes)
- | finish_primitive _ _ (Constrains _) = Constrains []
- | finish_primitive _ close (Assumes asms) = close (Assumes asms)
- | finish_primitive _ close (Defines defs) = close (Defines defs)
- | finish_primitive _ _ (Notes facts) = Notes facts;
+in
-fun finish_inst ctxt (loc, (prfx, inst)) =
- let
- val thy = Proof_Context.theory_of ctxt;
- val (parm_names, parm_types) = Locale.params_of thy loc |> map #1 |> split_list;
- val (morph, _) = inst_morph (parm_names, parm_types) (prfx, inst) ctxt;
- in (loc, morph) end;
+fun finish_elem _ parms _ (Fixes fixes) = Fixes (finish_fixes parms fixes)
+ | finish_elem _ _ _ (Constrains _) = Constrains []
+ | finish_elem ctxts parms do_close (Assumes asms) = closeup ctxts parms do_close (Assumes asms)
+ | finish_elem ctxts parms do_close (Defines defs) = closeup ctxts parms do_close (Defines defs)
+ | finish_elem _ _ _ (Notes facts) = Notes facts;
-fun finish_elem ctxt parms do_close elem =
- finish_primitive parms (closeup ctxt parms do_close) elem;
-
-fun finish ctxt parms do_close insts elems =
- let
- val deps = map (finish_inst ctxt) insts;
- val elems' = map (finish_elem ctxt parms do_close) elems;
- in (deps, elems') end;
+end;
(** Process full context statement: instantiations + elements + conclusion **)
@@ -399,9 +400,10 @@
val (Ts, ctxt7) = fold_map Proof_Context.inferred_param xs ctxt6;
val parms = xs ~~ Ts; (* params from expression and elements *)
- val Fixes fors' = finish_primitive parms I (Fixes fors);
+ val fors' = finish_fixes parms fors;
val fixed = map (fn (b, SOME T, mx) => ((Binding.name_of b, T), mx)) fors';
- val (deps, elems'') = finish ctxt6 parms do_close insts elems';
+ val deps = map (finish_inst ctxt6) insts;
+ val elems'' = map (finish_elem (ctxt1, ctxt6) parms do_close) elems';
in ((fixed, deps, elems'', concl), (parms, ctxt7)) end
@@ -428,12 +430,12 @@
fun prep_statement prep activate raw_elems raw_concl context =
let
- val ((_, _, elems, concl), _) =
- prep {strict = true, do_close = false, fixed_frees = true}
+ val ((_, _, elems, concl), _) =
+ prep {strict = true, do_close = false, fixed_frees = true}
([], []) I raw_elems raw_concl context;
- val (_, context') = context |>
- Proof_Context.set_stmt true |>
- fold_map activate elems;
+ val (_, context') = context
+ |> Proof_Context.set_stmt true
+ |> fold_map activate elems;
in (concl, context') end;
in
@@ -613,11 +615,14 @@
(* achieve plain syntax for locale predicates (without "PROP") *)
-fun aprop_tr' n c = (Lexicon.mark_const c, fn ctxt => fn args =>
- if length args = n then
- Syntax.const "_aprop" $ (* FIXME avoid old-style early externing (!??) *)
- Term.list_comb (Syntax.free (Proof_Context.extern_const ctxt c), args)
- else raise Match);
+fun aprop_tr' n c =
+ let
+ val c' = Lexicon.mark_const c;
+ fun tr' T args =
+ if T <> dummyT andalso length args = n
+ then Syntax.const "_aprop" $ Term.list_comb (Syntax.const c', args)
+ else raise Match;
+ in (c', tr') end;
(* define one predicate including its intro rule and axioms
- binding: predicate name
@@ -647,7 +652,7 @@
val ([pred_def], defs_thy) =
thy
- |> bodyT = propT ? Sign.add_advanced_trfuns ([], [], [aprop_tr' (length args) name], [])
+ |> bodyT = propT ? Sign.add_trfunsT [aprop_tr' (length args) name]
|> Sign.declare_const_global ((Binding.conceal binding, predT), NoSyn) |> snd
|> Global_Theory.add_defs false
[((Binding.conceal (Thm.def_binding binding), Logic.mk_equals (head, body)), [])];
--- a/src/Pure/Syntax/lexicon.ML Thu Oct 11 14:38:58 2012 +0200
+++ b/src/Pure/Syntax/lexicon.ML Thu Oct 11 21:02:19 2012 +0200
@@ -44,6 +44,7 @@
val tvarT: typ
val terminals: string list
val is_terminal: string -> bool
+ val literal_markup: string -> Markup.T
val report_of_token: token -> Position.report
val reported_token_range: Proof.context -> token -> string
val matching_tokens: token * token -> bool
@@ -188,25 +189,24 @@
(* markup *)
+fun literal_markup s =
+ if is_ascii_identifier s
+ then Isabelle_Markup.literal
+ else Isabelle_Markup.delimiter;
+
val token_kind_markup =
- fn Literal => Isabelle_Markup.literal
- | IdentSy => Markup.empty
- | LongIdentSy => Markup.empty
- | VarSy => Isabelle_Markup.var
- | TFreeSy => Isabelle_Markup.tfree
- | TVarSy => Isabelle_Markup.tvar
- | NumSy => Isabelle_Markup.numeral
- | FloatSy => Isabelle_Markup.numeral
- | XNumSy => Isabelle_Markup.numeral
- | StrSy => Isabelle_Markup.inner_string
- | Space => Markup.empty
- | Comment => Isabelle_Markup.inner_comment
- | EOF => Markup.empty;
+ fn VarSy => Isabelle_Markup.var
+ | TFreeSy => Isabelle_Markup.tfree
+ | TVarSy => Isabelle_Markup.tvar
+ | NumSy => Isabelle_Markup.numeral
+ | FloatSy => Isabelle_Markup.numeral
+ | XNumSy => Isabelle_Markup.numeral
+ | StrSy => Isabelle_Markup.inner_string
+ | Comment => Isabelle_Markup.inner_comment
+ | _ => Markup.empty;
fun report_of_token (Token (kind, s, (pos, _))) =
- let val markup =
- if kind = Literal andalso not (is_ascii_identifier s) then Isabelle_Markup.delimiter
- else token_kind_markup kind
+ let val markup = if kind = Literal then literal_markup s else token_kind_markup kind
in (pos, markup) end;
fun reported_token_range ctxt tok =
--- a/src/Pure/Syntax/printer.ML Thu Oct 11 14:38:58 2012 +0200
+++ b/src/Pure/Syntax/printer.ML Thu Oct 11 21:02:19 2012 +0200
@@ -92,8 +92,7 @@
datatype symb =
Arg of int |
TypArg of int |
- String of string |
- Space of string |
+ String of bool * string |
Break of int |
Block of int * symb list;
@@ -113,11 +112,12 @@
(if Lexicon.is_terminal s then 1000 else p);
fun xsyms_to_syms (Syntax_Ext.Delim s :: xsyms) =
- apfst (cons (String s)) (xsyms_to_syms xsyms)
+ apfst (cons (String (not (exists Symbol.is_block_ctrl (Symbol.explode s)), s)))
+ (xsyms_to_syms xsyms)
| xsyms_to_syms (Syntax_Ext.Argument s_p :: xsyms) =
apfst (cons (arg s_p)) (xsyms_to_syms xsyms)
| xsyms_to_syms (Syntax_Ext.Space s :: xsyms) =
- apfst (cons (Space s)) (xsyms_to_syms xsyms)
+ apfst (cons (String (false, s))) (xsyms_to_syms xsyms)
| xsyms_to_syms (Syntax_Ext.Bg i :: xsyms) =
let
val (bsyms, xsyms') = xsyms_to_syms xsyms;
@@ -133,7 +133,6 @@
fun nargs (Arg _ :: syms) = nargs syms + 1
| nargs (TypArg _ :: syms) = nargs syms + 1
| nargs (String _ :: syms) = nargs syms
- | nargs (Space _ :: syms) = nargs syms
| nargs (Break _ :: syms) = nargs syms
| nargs (Block (_, bsyms) :: syms) = nargs syms + nargs bsyms
| nargs [] = 0;
@@ -202,17 +201,14 @@
(pretty true curried (Config.put pretty_priority p ctxt)
tabs trf markup_trans markup_extern t @ Ts, args')
end
- | synT m (String s :: symbs, args) =
+ | synT m (String (do_mark, s) :: symbs, args) =
let
val (Ts, args') = synT m (symbs, args);
val T =
- if exists Symbol.is_block_ctrl (Symbol.explode s)
- then Pretty.str s
- else Pretty.marks_str (m, s);
+ if do_mark
+ then Pretty.marks_str (m @ [Lexicon.literal_markup s], s)
+ else Pretty.str s;
in (T :: Ts, args') end
- | synT m (Space s :: symbs, args) =
- let val (Ts, args') = synT m (symbs, args);
- in (Pretty.str s :: Ts, args') end
| synT m (Block (i, bsymbs) :: symbs, args) =
let
val (bTs, args') = synT m (bsymbs, args);
@@ -229,7 +225,7 @@
and parT m (pr, args, p, p': int) = #1 (synT m
(if p > p' orelse (show_brackets andalso p' <> 1000 andalso not (is_chain pr))
- then [Block (1, Space "(" :: pr @ [Space ")"])]
+ then [Block (1, String (false, "(") :: pr @ [String (false, ")")])]
else pr, args))
and atomT a = Pretty.marks_str (markup_extern a)
--- a/src/Tools/jEdit/src/isabelle_rendering.scala Thu Oct 11 14:38:58 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_rendering.scala Thu Oct 11 21:02:19 2012 +0200
@@ -211,10 +211,10 @@
Text.Info(snapshot.convert(info_range), Hyperlink(jedit_file, 0, 0)) :: links
case (links, Text.Info(info_range, XML.Elem(Markup(Isabelle_Markup.ENTITY, props), _)))
- if (props.find(
+ if !props.exists(
{ case (Markup.KIND, Isabelle_Markup.ML_OPEN) => true
case (Markup.KIND, Isabelle_Markup.ML_STRUCT) => true
- case _ => false }).isEmpty) =>
+ case _ => false }) =>
props match {
case Position.Def_Line_File(line, name) if Path.is_ok(name) =>