# HG changeset patch # User wenzelm # Date 1349982139 -7200 # Node ID be66949288a2affe9707296e79704fde763b6bd8 # Parent bb5db3d1d6dda3fb049e2cdd1786f4a2ad676ffa# Parent d15fe10593ff52c842efe4f6a0293682d58b5217 merged diff -r bb5db3d1d6dd -r be66949288a2 src/Pure/General/name_space.ML --- 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 = diff -r bb5db3d1d6dd -r be66949288a2 src/Pure/Isar/expression.ML --- 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)), [])]; diff -r bb5db3d1d6dd -r be66949288a2 src/Pure/Syntax/lexicon.ML --- 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 = diff -r bb5db3d1d6dd -r be66949288a2 src/Pure/Syntax/printer.ML --- 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) diff -r bb5db3d1d6dd -r be66949288a2 src/Tools/jEdit/src/isabelle_rendering.scala --- 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) =>