--- a/src/Pure/General/markup.ML Sun Mar 27 17:32:25 2011 +0200
+++ b/src/Pure/General/markup.ML Sun Mar 27 21:44:10 2011 +0200
@@ -16,7 +16,7 @@
val name: string -> T -> T
val kindN: string
val bindingN: string val binding: string -> T
- val entityN: string val entity: string -> T
+ val entityN: string val entity: string -> string -> T
val defN: string
val refN: string
val lineN: string
@@ -174,7 +174,9 @@
(* formal entities *)
val (bindingN, binding) = markup_string "binding" nameN;
-val (entityN, entity) = markup_string "entity" nameN;
+
+val entityN = "entity";
+fun entity kind name = (entityN, [(kindN, kind), (nameN, name)]);
val defN = "def";
val refN = "ref";
@@ -218,7 +220,7 @@
val (fixed_declN, fixed_decl) = markup_string "fixed_decl" nameN;
val (fixedN, fixed) = markup_string "fixed" nameN;
val (const_declN, const_decl) = markup_string "const_decl" nameN;
-val (constN, const) = markup_string "const" nameN;
+val (constN, const) = markup_string "constant" nameN;
val (fact_declN, fact_decl) = markup_string "fact_decl" nameN;
val (factN, fact) = markup_string "fact" nameN;
val (dynamic_factN, dynamic_fact) = markup_string "dynamic_fact" nameN;
--- a/src/Pure/General/markup.scala Sun Mar 27 17:32:25 2011 +0200
+++ b/src/Pure/General/markup.scala Sun Mar 27 21:44:10 2011 +0200
@@ -84,7 +84,10 @@
/* misc properties */
val NAME = "name"
+ val Name = new Property(NAME)
+
val KIND = "kind"
+ val Kind = new Property(KIND)
/* formal entities */
@@ -129,7 +132,7 @@
val FIXED_DECL = "fixed_decl"
val FIXED = "fixed"
val CONST_DECL = "const_decl"
- val CONST = "const"
+ val CONST = "constant"
val FACT_DECL = "fact_decl"
val FACT = "fact"
val DYNAMIC_FACT = "dynamic_fact"
--- a/src/Pure/General/name_space.ML Sun Mar 27 17:32:25 2011 +0200
+++ b/src/Pure/General/name_space.ML Sun Mar 27 21:44:10 2011 +0200
@@ -24,6 +24,7 @@
val kind_of: T -> string
val the_entry: T -> string ->
{concealed: bool, group: serial option, theory_name: string, pos: Position.T, id: serial}
+ val markup_entry: T -> string -> Markup.T
val is_concealed: T -> string -> bool
val intern: T -> xstring -> string
val extern_flags: {long_names: bool, short_names: bool, unique_names: bool} ->
@@ -79,15 +80,18 @@
pos: Position.T,
id: serial};
-fun str_of_entry def (name, {pos, id, ...}: entry) =
+fun entry_markup def kind (name, {pos, id, ...}: entry) =
let
val occurrence = (if def then Markup.defN else Markup.refN, string_of_int id);
val props = occurrence :: Position.properties_of pos;
- in Markup.markup (Markup.properties props (Markup.entity name)) name end;
+ in Markup.properties props (Markup.entity kind name) end;
+
+fun print_entry def kind (name, entry) =
+ quote (Markup.markup (entry_markup def kind (name, entry)) name);
fun err_dup kind entry1 entry2 =
error ("Duplicate " ^ kind ^ " declaration " ^
- quote (str_of_entry true entry1) ^ " vs. " ^ quote (str_of_entry true entry2));
+ print_entry true kind entry1 ^ " vs. " ^ print_entry true kind entry2);
(* datatype T *)
@@ -117,6 +121,11 @@
NONE => error ("Unknown " ^ kind ^ " " ^ quote name)
| SOME (_, entry) => entry);
+fun markup_entry (Name_Space {kind, entries, ...}) name =
+ (case Symtab.lookup entries name of
+ NONE => Markup.malformed
+ | SOME (_, entry) => entry_markup false kind (name, entry));
+
fun is_concealed space name = #concealed (the_entry space name);
--- a/src/Pure/Isar/proof_context.ML Sun Mar 27 17:32:25 2011 +0200
+++ b/src/Pure/Isar/proof_context.ML Sun Mar 27 21:44:10 2011 +0200
@@ -65,7 +65,7 @@
val allow_dummies: Proof.context -> Proof.context
val check_tvar: Proof.context -> indexname * sort -> indexname * sort
val check_tfree: Proof.context -> string * sort -> string * sort
- val decode_term: Proof.context -> term -> term
+ val decode_term: Proof.context -> term -> (Position.T * Markup.T) list * term
val standard_infer_types: Proof.context -> term list -> term list
val read_term_pattern: Proof.context -> string -> term
val read_term_schematic: Proof.context -> string -> term
@@ -261,6 +261,7 @@
fun default_sort ctxt = the_default (Type.defaultS (tsig_of ctxt)) o Variable.def_sort ctxt;
val consts_of = #1 o #consts o rep_context;
+val const_space = Consts.space_of o consts_of;
val the_const_constraint = Consts.the_constraint o consts_of;
val facts_of = #facts o rep_context;
@@ -664,15 +665,16 @@
in
-fun term_context ctxt =
- {get_sort = get_sort ctxt,
- map_const = fn a => ((true, #1 (Term.dest_Const (read_const_proper ctxt false a)))
- handle ERROR _ => (false, Consts.intern (consts_of ctxt) a)),
- map_free = intern_skolem ctxt (Variable.def_type ctxt false)};
+fun term_context ctxt : Syntax.term_context =
+ {get_sort = get_sort ctxt,
+ get_const = fn a => ((true, #1 (Term.dest_Const (read_const_proper ctxt false a)))
+ handle ERROR _ => (false, Consts.intern (consts_of ctxt) a)),
+ get_free = intern_skolem ctxt (Variable.def_type ctxt false),
+ markup_const = Name_Space.markup_entry (const_space ctxt),
+ markup_free = fn x => Markup.name x Markup.free,
+ markup_var = fn xi => Markup.name (Term.string_of_vname xi) Markup.var};
-fun decode_term ctxt =
- let val {get_sort, map_const, map_free} = term_context ctxt
- in Syntax.decode_term get_sort map_const map_free end;
+val decode_term = Syntax.decode_term o term_context;
end;
@@ -757,8 +759,6 @@
fun parse_term T ctxt text =
let
- val {get_sort, map_const, map_free} = term_context ctxt;
-
val (T', _) = Type_Infer.paramify_dummies T 0;
val (markup, kind) =
if T' = propT then (Markup.prop, "proposition") else (Markup.term, "term");
@@ -775,9 +775,8 @@
fun check t = (Syntax.check_term ctxt (Type.constraint T' t); NONE)
handle ERROR msg => SOME msg;
val t =
- Syntax.standard_parse_term check get_sort map_const map_free
- ctxt (syn_of ctxt) root (syms, pos)
- handle ERROR msg => parse_failed ctxt pos msg kind;
+ Syntax.standard_parse_term check (term_context ctxt) ctxt (syn_of ctxt) root (syms, pos)
+ handle ERROR msg => parse_failed ctxt pos msg kind;
in t end;
--- a/src/Pure/Syntax/mixfix.ML Sun Mar 27 17:32:25 2011 +0200
+++ b/src/Pure/Syntax/mixfix.ML Sun Mar 27 21:44:10 2011 +0200
@@ -109,7 +109,7 @@
| mfix_of (t, ty, Infix (sy, p)) = SOME (mk_infix sy ty t (p + 1) (p + 1) p)
| mfix_of (t, ty, Infixl (sy, p)) = SOME (mk_infix sy ty t p (p + 1) p)
| mfix_of (t, ty, Infixr (sy, p)) = SOME (mk_infix sy ty t (p + 1) p p)
- | mfix_of (t, _, _) = error ("Bad mixfix declaration for " ^ quote t); (* FIXME printable t (!?) *)
+ | mfix_of (t, _, _) = error ("Bad mixfix declaration for " ^ quote t);
fun check_args (_, ty, _) (SOME (mfix as Syn_Ext.Mfix (sy, _, _, _, _))) =
if length (Term.binder_types ty) = Syn_Ext.mfix_args sy then ()
@@ -145,7 +145,7 @@
| mfix_of (c, ty, Infixr (sy, p)) = mk_infix sy ty c (p + 1) p p
| mfix_of (c, ty, Binder (sy, p, q)) =
[Syn_Ext.Mfix ("(3" ^ sy ^ "_./ _)", binder_typ c ty, (binder_name c), [0, p], q)]
- | mfix_of (c, _, _) = error ("Bad mixfix declaration for " ^ quote c); (* FIXME printable c (!?) *)
+ | mfix_of (c, _, _) = error ("Bad mixfix declaration for " ^ quote c);
fun binder (c, _, Binder _) = SOME (binder_name c, c)
| binder _ = NONE;
--- a/src/Pure/Syntax/syntax.ML Sun Mar 27 17:32:25 2011 +0200
+++ b/src/Pure/Syntax/syntax.ML Sun Mar 27 21:44:10 2011 +0200
@@ -116,10 +116,8 @@
val ambiguity_level_raw: Config.raw
val ambiguity_level: int Config.T
val ambiguity_limit: int Config.T
- val standard_parse_term: (term -> string option) ->
- (((string * int) * sort) list -> string * int -> Term.sort) ->
- (string -> bool * string) -> (string -> string option) -> Proof.context ->
- syntax -> string -> Symbol_Pos.T list * Position.T -> term
+ val standard_parse_term: (term -> string option) -> term_context ->
+ Proof.context -> syntax -> string -> Symbol_Pos.T list * Position.T -> term
val standard_parse_typ: Proof.context -> syntax ->
((indexname * sort) list -> indexname -> sort) -> Symbol_Pos.T list * Position.T -> typ
val standard_parse_sort: Proof.context -> syntax -> Symbol_Pos.T list * Position.T -> sort
@@ -756,22 +754,25 @@
(* read terms *)
+fun report_result ctxt (reports, res) =
+ (List.app (fn (pos, m) => Context_Position.report ctxt pos m) reports; res);
+
(*brute-force disambiguation via type-inference*)
-fun disambig _ _ [t] = t
- | disambig ctxt check ts =
+fun disambig ctxt _ [arg] = report_result ctxt arg
+ | disambig ctxt check args =
let
val level = Config.get ctxt ambiguity_level;
val limit = Config.get ctxt ambiguity_limit;
- val ambiguity = length ts;
+ val ambiguity = length args;
fun ambig_msg () =
if ambiguity > 1 andalso ambiguity <= level then
"Got more than one parse tree.\n\
\Retry with smaller syntax_ambiguity_level for more information."
else "";
- val errs = Par_List.map_name "Syntax.disambig" check ts;
- val results = map_filter (fn (t, NONE) => SOME t | _ => NONE) (ts ~~ errs);
+ val errs = Par_List.map_name "Syntax.disambig" (check o snd) args;
+ val results = map_filter (fn (arg, NONE) => SOME arg | _ => NONE) (args ~~ errs);
val len = length results;
val show_term = string_of_term (Config.put Printer.show_brackets true ctxt);
@@ -782,16 +783,16 @@
Context_Position.if_visible ctxt warning
"Fortunately, only one parse tree is type correct.\n\
\You may still want to disambiguate your grammar or your input."
- else (); hd results)
+ else (); report_result ctxt (hd results))
else cat_error (ambig_msg ()) (cat_lines
(("Ambiguous input, " ^ string_of_int len ^ " terms are type correct" ^
(if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
- map show_term (take limit results)))
+ map (show_term o snd) (take limit results)))
end;
-fun standard_parse_term check get_sort map_const map_free ctxt syn root (syms, pos) =
+fun standard_parse_term check term_ctxt ctxt syn root (syms, pos) =
read ctxt syn root (syms, pos)
- |> map (Type_Ext.decode_term get_sort map_const map_free)
+ |> map (Type_Ext.decode_term term_ctxt)
|> disambig ctxt check;
--- a/src/Pure/Syntax/type_ext.ML Sun Mar 27 17:32:25 2011 +0200
+++ b/src/Pure/Syntax/type_ext.ML Sun Mar 27 21:44:10 2011 +0200
@@ -12,8 +12,8 @@
val is_position: term -> bool
val strip_positions: term -> term
val strip_positions_ast: Ast.ast -> Ast.ast
- val decode_term: (((string * int) * sort) list -> string * int -> sort) ->
- (string -> bool * string) -> (string -> string option) -> term -> term
+ type term_context
+ val decode_term: term_context -> term -> (Position.T * Markup.T) list * term
val term_of_typ: bool -> typ -> term
val no_brackets: unit -> bool
val no_type_brackets: unit -> bool
@@ -106,8 +106,10 @@
(* positions *)
-fun is_position (Free (x, _)) = is_some (Lexicon.decode_position x)
- | is_position _ = false;
+fun decode_position (Free (x, _)) = Lexicon.decode_position x
+ | decode_position _ = NONE;
+
+val is_position = is_some o decode_position;
fun strip_positions ((t as Const (c, _)) $ u $ v) =
if (c = "_constrain" orelse c = "_constrainAbs") andalso is_position v
@@ -127,35 +129,69 @@
(* decode_term -- transform parse tree into raw term *)
-fun decode_term get_sort map_const map_free tm =
+fun markup_bound def id =
+ Markup.properties [(if def then Markup.defN else Markup.refN, id)] Markup.bound;
+
+type term_context =
+ {get_sort: (indexname * sort) list -> indexname -> sort,
+ get_const: string -> bool * string,
+ get_free: string -> string option,
+ markup_const: string -> Markup.T,
+ markup_free: string -> Markup.T,
+ markup_var: indexname -> Markup.T};
+
+fun decode_term (term_context: term_context) tm =
let
+ val {get_sort, get_const, get_free, markup_const, markup_free, markup_var} = term_context;
val decodeT = typ_of_term (get_sort (term_sorts tm));
- fun decode (Const ("_constrain", _) $ t $ typ) =
- if is_position typ then decode t
- else Type.constraint (decodeT typ) (decode t)
- | decode (Const ("_constrainAbs", _) $ t $ typ) =
- if is_position typ then decode t
- else Type.constraint (decodeT typ --> dummyT) (decode t)
- | decode (Abs (x, T, t)) = Abs (x, T, decode t)
- | decode (t $ u) = decode t $ decode u
- | decode (Const (a, T)) =
+ val reports = Unsynchronized.ref ([]: (Position.T * Markup.T) list);
+ fun report [] _ _ = ()
+ | report ps markup x =
+ let val m = markup x
+ in Unsynchronized.change reports (fold (fn p => cons (p, m)) ps) end;
+
+ fun decode ps qs bs (Const ("_constrain", _) $ t $ typ) =
+ (case decode_position typ of
+ SOME p => decode (p :: ps) qs bs t
+ | NONE => Type.constraint (decodeT typ) (decode ps qs bs t))
+ | decode ps qs bs (Const ("_constrainAbs", _) $ t $ typ) =
+ (case decode_position typ of
+ SOME q => decode ps (q :: qs) bs t
+ | NONE => Type.constraint (decodeT typ --> dummyT) (decode ps qs bs t))
+ | decode _ qs bs (Abs (x, T, t)) =
+ let
+ val id = serial_string ();
+ val _ = report qs (markup_bound true) id;
+ in Abs (x, T, decode [] [] (id :: bs) t) end
+ | decode _ _ bs (t $ u) = decode [] [] bs t $ decode [] [] bs u
+ | decode ps _ _ (Const (a, T)) =
(case try Lexicon.unmark_fixed a of
- SOME x => Free (x, T)
+ SOME x => (report ps markup_free x; Free (x, T))
| NONE =>
- let val c =
- (case try Lexicon.unmark_const a of
- SOME c => c
- | NONE => snd (map_const a))
+ let
+ val c =
+ (case try Lexicon.unmark_const a of
+ SOME c => c
+ | NONE => snd (get_const a));
+ val _ = report ps markup_const c;
in Const (c, T) end)
- | decode (Free (a, T)) =
- (case (map_free a, map_const a) of
- (SOME x, _) => Free (x, T)
- | (_, (true, c)) => Const (c, T)
- | (_, (false, c)) => (if Long_Name.is_qualified c then Const else Free) (c, T))
- | decode (Var (xi, T)) = Var (xi, T)
- | decode (t as Bound _) = t;
- in decode tm end;
+ | decode ps _ _ (Free (a, T)) =
+ (case (get_free a, get_const a) of
+ (SOME x, _) => (report ps markup_free x; Free (x, T))
+ | (_, (true, c)) => (report ps markup_const c; Const (c, T))
+ | (_, (false, c)) =>
+ if Long_Name.is_qualified c
+ then (report ps markup_const c; Const (c, T))
+ else (report ps markup_free c; Free (c, T)))
+ | decode ps _ _ (Var (xi, T)) = (report ps markup_var xi; Var (xi, T))
+ | decode ps _ bs (t as Bound i) =
+ (case try (nth bs) i of
+ SOME id => (report ps (markup_bound false) id; t)
+ | NONE => t);
+
+ val tm' = decode [] [] [] tm;
+ in (! reports, tm') end;
--- a/src/Tools/jEdit/src/jedit/isabelle_markup.scala Sun Mar 27 17:32:25 2011 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_markup.scala Sun Mar 27 21:44:10 2011 +0200
@@ -144,7 +144,7 @@
Markup.FIXED_DECL -> FUNCTION,
Markup.FIXED -> NULL,
Markup.CONST_DECL -> FUNCTION,
- Markup.CONST -> NULL,
+ Markup.CONST -> LITERAL2,
Markup.FACT_DECL -> FUNCTION,
Markup.FACT -> NULL,
Markup.DYNAMIC_FACT -> LABEL,
@@ -152,10 +152,10 @@
Markup.LOCAL_FACT -> NULL,
// inner syntax
Markup.TFREE -> NULL,
- Markup.FREE -> NULL,
+ Markup.FREE -> MARKUP,
Markup.TVAR -> NULL,
Markup.SKOLEM -> NULL,
- Markup.BOUND -> NULL,
+ Markup.BOUND -> LABEL,
Markup.VAR -> NULL,
Markup.NUM -> DIGIT,
Markup.FLOAT -> DIGIT,
@@ -204,6 +204,9 @@
case Text.Info(_, XML.Elem(Markup(Markup.COMMAND, List((Markup.NAME, name))), _))
if syntax.keyword_kind(name).isDefined => command_style(syntax.keyword_kind(name).get)
+ case Text.Info(_, XML.Elem(Markup(Markup.ENTITY, Markup.Kind(kind)), _))
+ if token_style(kind) != Token.NULL => token_style(kind)
+
case Text.Info(_, XML.Elem(Markup(name, _), _))
if token_style(name) != Token.NULL => token_style(name)
}