more accurate markup for syntax consts, notably binders which point back to the original logical entity;
authorwenzelm
Fri Apr 08 22:40:29 2011 +0200 (2011-04-08)
changeset 42298d622145603ee
parent 42297 140f283266b7
child 42299 06e93f257d0e
more accurate markup for syntax consts, notably binders which point back to the original logical entity;
tuned;
src/Pure/ML/ml_antiquote.ML
src/Pure/Syntax/mixfix.ML
src/Pure/Syntax/syntax.ML
src/Pure/Syntax/syntax_ext.ML
src/Pure/Syntax/syntax_phases.ML
     1.1 --- a/src/Pure/ML/ml_antiquote.ML	Fri Apr 08 21:11:29 2011 +0200
     1.2 +++ b/src/Pure/ML/ml_antiquote.ML	Fri Apr 08 22:40:29 2011 +0200
     1.3 @@ -151,7 +151,8 @@
     1.4  
     1.5  val _ = inline "syntax_const"
     1.6    (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (c, pos)) =>
     1.7 -    if Syntax.is_const (ProofContext.syn_of ctxt) c then ML_Syntax.print_string c
     1.8 +    if is_some (Syntax.lookup_const (ProofContext.syn_of ctxt) c)
     1.9 +    then ML_Syntax.print_string c
    1.10      else error ("Unknown syntax const: " ^ quote c ^ Position.str_of pos)));
    1.11  
    1.12  val _ = inline "const"
     2.1 --- a/src/Pure/Syntax/mixfix.ML	Fri Apr 08 21:11:29 2011 +0200
     2.2 +++ b/src/Pure/Syntax/mixfix.ML	Fri Apr 08 22:40:29 2011 +0200
     2.3 @@ -110,8 +110,8 @@
     2.4  
     2.5      val mfix = map mfix_of type_decls;
     2.6      val _ = map2 check_args type_decls mfix;
     2.7 -    val xconsts = map #1 type_decls;
     2.8 -  in Syntax_Ext.syn_ext (map_filter I mfix) xconsts ([], [], [], []) ([], []) end;
     2.9 +    val consts = map (fn (t, _, _) => (t, "")) type_decls;
    2.10 +  in Syntax_Ext.syn_ext (map_filter I mfix) consts ([], [], [], []) ([], []) end;
    2.11  
    2.12  
    2.13  (* syn_ext_consts *)
    2.14 @@ -143,15 +143,16 @@
    2.15        | binder _ = NONE;
    2.16  
    2.17      val mfix = maps mfix_of const_decls;
    2.18 -    val xconsts = map #1 const_decls;
    2.19      val binders = map_filter binder const_decls;
    2.20      val binder_trs = binders
    2.21        |> map (Syntax_Ext.stamp_trfun binder_stamp o apsnd K o Syntax_Trans.mk_binder_tr);
    2.22      val binder_trs' = binders
    2.23        |> map (Syntax_Ext.stamp_trfun binder_stamp o
    2.24            apsnd (K o Syntax_Trans.non_typed_tr') o Syntax_Trans.mk_binder_tr' o swap);
    2.25 +
    2.26 +    val consts = binders @ map (fn (c, _, _) => (c, "")) const_decls;
    2.27    in
    2.28 -    Syntax_Ext.syn_ext' is_logtype mfix xconsts ([], binder_trs, binder_trs', []) ([], [])
    2.29 +    Syntax_Ext.syn_ext' is_logtype mfix consts ([], binder_trs, binder_trs', []) ([], [])
    2.30    end;
    2.31  
    2.32  end;
     3.1 --- a/src/Pure/Syntax/syntax.ML	Fri Apr 08 21:11:29 2011 +0200
     3.2 +++ b/src/Pure/Syntax/syntax.ML	Fri Apr 08 22:40:29 2011 +0200
     3.3 @@ -94,7 +94,7 @@
     3.4    val pp_global: theory -> Pretty.pp
     3.5    type syntax
     3.6    val eq_syntax: syntax * syntax -> bool
     3.7 -  val is_const: syntax -> string -> bool
     3.8 +  val lookup_const: syntax -> string -> string option
     3.9    val is_keyword: syntax -> string -> bool
    3.10    val tokenize: syntax -> bool -> Symbol_Pos.T list -> Lexicon.token list
    3.11    val parse: Proof.context -> syntax -> string -> Lexicon.token list -> Parser.parsetree list
    3.12 @@ -458,7 +458,7 @@
    3.13      input: Syntax_Ext.xprod list,
    3.14      lexicon: Scan.lexicon,
    3.15      gram: Parser.gram,
    3.16 -    consts: string list,
    3.17 +    consts: string Symtab.table,
    3.18      prmodes: string list,
    3.19      parse_ast_trtab: ((Proof.context -> Ast.ast list -> Ast.ast) * stamp) Symtab.table,
    3.20      parse_ruletab: ruletab,
    3.21 @@ -470,7 +470,7 @@
    3.22  
    3.23  fun eq_syntax (Syntax (_, s1), Syntax (_, s2)) = s1 = s2;
    3.24  
    3.25 -fun is_const (Syntax ({consts, ...}, _)) c = member (op =) consts c;
    3.26 +fun lookup_const (Syntax ({consts, ...}, _)) = Symtab.lookup consts;
    3.27  fun is_keyword (Syntax ({lexicon, ...}, _)) = Scan.is_literal lexicon o Symbol.explode;
    3.28  fun tokenize (Syntax ({lexicon, ...}, _)) = Lexicon.tokenize lexicon;
    3.29  fun parse ctxt (Syntax ({gram, ...}, _)) = Parser.parse ctxt gram;
    3.30 @@ -495,7 +495,7 @@
    3.31    ({input = [],
    3.32      lexicon = Scan.empty_lexicon,
    3.33      gram = Parser.empty_gram,
    3.34 -    consts = [],
    3.35 +    consts = Symtab.empty,
    3.36      prmodes = [],
    3.37      parse_ast_trtab = Symtab.empty,
    3.38      parse_ruletab = Symtab.empty,
    3.39 @@ -508,6 +508,11 @@
    3.40  
    3.41  (* update_syntax *)
    3.42  
    3.43 +fun update_const (c, b) tab =
    3.44 +  if c = "" orelse (b = "" andalso (Lexicon.is_marked c orelse Symtab.defined tab c))
    3.45 +  then tab
    3.46 +  else Symtab.update (c, b) tab;
    3.47 +
    3.48  fun update_syntax (mode, inout) syn_ext (Syntax (tabs, _)) =
    3.49    let
    3.50      val {input, lexicon, gram, consts = consts1, prmodes, parse_ast_trtab, parse_ruletab,
    3.51 @@ -523,7 +528,7 @@
    3.52      ({input = new_xprods @ input,
    3.53        lexicon = fold Scan.extend_lexicon (Syntax_Ext.delims_of new_xprods) lexicon,
    3.54        gram = Parser.extend_gram new_xprods gram,
    3.55 -      consts = Library.merge (op =) (consts1, filter_out Lexicon.is_marked consts2),
    3.56 +      consts = fold update_const consts2 consts1,
    3.57        prmodes = insert (op =) mode prmodes,
    3.58        parse_ast_trtab =
    3.59          update_trtab "parse ast translation" (if_inout parse_ast_translation) parse_ast_trtab,
    3.60 @@ -582,7 +587,7 @@
    3.61      ({input = Library.merge (op =) (input1, input2),
    3.62        lexicon = Scan.merge_lexicons (lexicon1, lexicon2),
    3.63        gram = Parser.merge_gram (gram1, gram2),
    3.64 -      consts = sort_distinct string_ord (consts1 @ consts2),
    3.65 +      consts = Symtab.merge (K true) (consts1, consts2),
    3.66        prmodes = Library.merge (op =) (prmodes1, prmodes2),
    3.67        parse_ast_trtab =
    3.68          merge_trtabs "parse ast translation" parse_ast_trtab1 parse_ast_trtab2,
    3.69 @@ -627,8 +632,8 @@
    3.70  
    3.71  fun pretty_trans (Syntax (tabs, _)) =
    3.72    let
    3.73 -    fun pretty_trtab name tab =
    3.74 -      pretty_strs_qs name (Symtab.keys tab);
    3.75 +    fun pretty_tab name tab =
    3.76 +      pretty_strs_qs name (sort_strings (Symtab.keys tab));
    3.77  
    3.78      fun pretty_ruletab name tab =
    3.79        Pretty.big_list name (map Ast.pretty_rule (dest_ruletab tab));
    3.80 @@ -636,13 +641,13 @@
    3.81      val {consts, parse_ast_trtab, parse_ruletab, parse_trtab, print_trtab,
    3.82        print_ruletab, print_ast_trtab, ...} = tabs;
    3.83    in
    3.84 -    [pretty_strs_qs "consts:" consts,
    3.85 -      pretty_trtab "parse_ast_translation:" parse_ast_trtab,
    3.86 -      pretty_ruletab "parse_rules:" parse_ruletab,
    3.87 -      pretty_trtab "parse_translation:" parse_trtab,
    3.88 -      pretty_trtab "print_translation:" print_trtab,
    3.89 -      pretty_ruletab "print_rules:" print_ruletab,
    3.90 -      pretty_trtab "print_ast_translation:" print_ast_trtab]
    3.91 +   [pretty_tab "consts:" consts,
    3.92 +    pretty_tab "parse_ast_translation:" parse_ast_trtab,
    3.93 +    pretty_ruletab "parse_rules:" parse_ruletab,
    3.94 +    pretty_tab "parse_translation:" parse_trtab,
    3.95 +    pretty_tab "print_translation:" print_trtab,
    3.96 +    pretty_ruletab "print_rules:" print_ruletab,
    3.97 +    pretty_tab "print_ast_translation:" print_ast_trtab]
    3.98    end;
    3.99  
   3.100  in
     4.1 --- a/src/Pure/Syntax/syntax_ext.ML	Fri Apr 08 21:11:29 2011 +0200
     4.2 +++ b/src/Pure/Syntax/syntax_ext.ML	Fri Apr 08 22:40:29 2011 +0200
     4.3 @@ -21,7 +21,7 @@
     4.4    datatype syn_ext =
     4.5      Syn_Ext of {
     4.6        xprods: xprod list,
     4.7 -      consts: string list,
     4.8 +      consts: (string * string) list,
     4.9        parse_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list,
    4.10        parse_rules: (Ast.ast * Ast.ast) list,
    4.11        parse_translation: (string * ((Proof.context -> term list -> term) * stamp)) list,
    4.12 @@ -32,18 +32,17 @@
    4.13    val mfix_args: string -> int
    4.14    val escape: string -> string
    4.15    val syn_ext': (string -> bool) -> mfix list ->
    4.16 -    string list -> (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list *
    4.17 +    (string * string) list -> (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list *
    4.18      (string * ((Proof.context -> term list -> term) * stamp)) list *
    4.19      (string * ((Proof.context -> typ -> term list -> term) * stamp)) list *
    4.20      (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list ->
    4.21      (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
    4.22 -  val syn_ext: mfix list -> string list ->
    4.23 +  val syn_ext: mfix list -> (string * string) list ->
    4.24      (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list *
    4.25      (string * ((Proof.context -> term list -> term) * stamp)) list *
    4.26      (string * ((Proof.context -> typ -> term list -> term) * stamp)) list *
    4.27      (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list ->
    4.28      (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
    4.29 -  val syn_ext_const_names: string list -> syn_ext
    4.30    val syn_ext_rules: (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
    4.31    val syn_ext_trfuns:
    4.32      (string * ((Ast.ast list -> Ast.ast) * stamp)) list *
    4.33 @@ -283,7 +282,7 @@
    4.34  datatype syn_ext =
    4.35    Syn_Ext of {
    4.36      xprods: xprod list,
    4.37 -    consts: string list,
    4.38 +    consts: (string * string) list,
    4.39      parse_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list,
    4.40      parse_rules: (Ast.ast * Ast.ast) list,
    4.41      parse_translation: (string * ((Proof.context -> term list -> term) * stamp)) list,
    4.42 @@ -301,12 +300,11 @@
    4.43  
    4.44      val (xprods, parse_rules') = map (mfix_to_xprod is_logtype) mfixes
    4.45        |> split_list |> apsnd (rev o flat);
    4.46 -    val mfix_consts =
    4.47 -      distinct (op =) (map (fn Mfix x => #3 x) mfixes @ map (fn XProd x => #3 x) xprods);
    4.48 +    val mfix_consts = map (fn Mfix x => (#3 x, "")) mfixes @ map (fn XProd x => (#3 x, "")) xprods;
    4.49    in
    4.50      Syn_Ext {
    4.51        xprods = xprods,
    4.52 -      consts = union (op =) consts mfix_consts,
    4.53 +      consts = mfix_consts @ consts,
    4.54        parse_ast_translation = parse_ast_translation,
    4.55        parse_rules = parse_rules' @ parse_rules,
    4.56        parse_translation = parse_translation,
    4.57 @@ -318,7 +316,6 @@
    4.58  
    4.59  val syn_ext = syn_ext' (K false);
    4.60  
    4.61 -fun syn_ext_const_names cs = syn_ext [] cs ([], [], [], []) ([], []);
    4.62  fun syn_ext_rules rules = syn_ext [] [] ([], [], [], []) rules;
    4.63  fun syn_ext_advanced_trfuns trfuns = syn_ext [] [] trfuns ([], []);
    4.64  
     5.1 --- a/src/Pure/Syntax/syntax_phases.ML	Fri Apr 08 21:11:29 2011 +0200
     5.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Fri Apr 08 22:40:29 2011 +0200
     5.3 @@ -18,6 +18,40 @@
     5.4  structure Syntax_Phases: SYNTAX_PHASES =
     5.5  struct
     5.6  
     5.7 +(** markup logical entities **)
     5.8 +
     5.9 +fun markup_class ctxt c =
    5.10 +  [Name_Space.markup_entry (Type.class_space (ProofContext.tsig_of ctxt)) c];
    5.11 +
    5.12 +fun markup_type ctxt c =
    5.13 +  [Name_Space.markup_entry (Type.type_space (ProofContext.tsig_of ctxt)) c];
    5.14 +
    5.15 +fun markup_const ctxt c =
    5.16 +  [Name_Space.markup_entry (Consts.space_of (ProofContext.consts_of ctxt)) c];
    5.17 +
    5.18 +fun markup_free ctxt x =
    5.19 +  [if can Name.dest_skolem x then Markup.skolem else Markup.free] @
    5.20 +  (if not (Variable.is_body ctxt) orelse Variable.is_fixed ctxt x then []
    5.21 +   else [Markup.hilite]);
    5.22 +
    5.23 +fun markup_var xi = [Markup.name (Term.string_of_vname xi) Markup.var];
    5.24 +
    5.25 +fun markup_bound def id =
    5.26 +  [Markup.properties [(if def then Markup.defN else Markup.refN, id)] Markup.bound];
    5.27 +
    5.28 +fun markup_entity ctxt c =
    5.29 +  (case Syntax.lookup_const (ProofContext.syn_of ctxt) c of
    5.30 +    SOME "" => []
    5.31 +  | SOME b => markup_entity ctxt b
    5.32 +  | NONE => c |> Lexicon.unmark
    5.33 +     {case_class = markup_class ctxt,
    5.34 +      case_type = markup_type ctxt,
    5.35 +      case_const = markup_const ctxt,
    5.36 +      case_fixed = markup_free ctxt,
    5.37 +      case_default = K []});
    5.38 +
    5.39 +
    5.40 +
    5.41  (** decode parse trees **)
    5.42  
    5.43  (* sort_of_term *)
    5.44 @@ -89,29 +123,10 @@
    5.45  
    5.46  (* parsetree_to_ast *)
    5.47  
    5.48 -fun markup_const ctxt c =
    5.49 -  [Name_Space.markup_entry (Consts.space_of (ProofContext.consts_of ctxt)) c];
    5.50 -
    5.51 -fun markup_free ctxt x =
    5.52 -  [if can Name.dest_skolem x then Markup.skolem else Markup.free] @
    5.53 -  (if not (Variable.is_body ctxt) orelse Variable.is_fixed ctxt x then []
    5.54 -   else [Markup.hilite]);
    5.55 -
    5.56  fun parsetree_to_ast ctxt constrain_pos trf parsetree =
    5.57    let
    5.58 -    val tsig = ProofContext.tsig_of ctxt;
    5.59 -
    5.60      val get_class = ProofContext.read_class ctxt;
    5.61      val get_type = #1 o dest_Type o ProofContext.read_type_name_proper ctxt false;
    5.62 -    fun markup_class c = [Name_Space.markup_entry (Type.class_space tsig) c];
    5.63 -    fun markup_type c = [Name_Space.markup_entry (Type.type_space tsig) c];
    5.64 -
    5.65 -    val markup_entity = Lexicon.unmark
    5.66 -     {case_class = markup_class,
    5.67 -      case_type = markup_type,
    5.68 -      case_const = markup_const ctxt,
    5.69 -      case_fixed = markup_free ctxt,
    5.70 -      case_default = K []};
    5.71  
    5.72      val reports = Unsynchronized.ref ([]: Position.reports);
    5.73      fun report pos = Position.reports reports [pos];
    5.74 @@ -124,12 +139,12 @@
    5.75      fun asts_of (Parser.Node ("_class_name", [Parser.Tip tok])) =
    5.76            let
    5.77              val c = get_class (Lexicon.str_of_token tok);
    5.78 -            val _ = report (Lexicon.pos_of_token tok) markup_class c;
    5.79 +            val _ = report (Lexicon.pos_of_token tok) (markup_class ctxt) c;
    5.80            in [Ast.Constant (Lexicon.mark_class c)] end
    5.81        | asts_of (Parser.Node ("_type_name", [Parser.Tip tok])) =
    5.82            let
    5.83              val c = get_type (Lexicon.str_of_token tok);
    5.84 -            val _ = report (Lexicon.pos_of_token tok) markup_type c;
    5.85 +            val _ = report (Lexicon.pos_of_token tok) (markup_type ctxt) c;
    5.86            in [Ast.Constant (Lexicon.mark_type c)] end
    5.87        | asts_of (Parser.Node ("_constrain_position", [pt as Parser.Tip tok])) =
    5.88            if constrain_pos then
    5.89 @@ -141,7 +156,7 @@
    5.90              val _ = pts |> List.app
    5.91                (fn Parser.Node _ => () | Parser.Tip tok =>
    5.92                  if Lexicon.valued_token tok then ()
    5.93 -                else report (Lexicon.pos_of_token tok) markup_entity a);
    5.94 +                else report (Lexicon.pos_of_token tok) (markup_entity ctxt) a);
    5.95            in [trans a (maps asts_of pts)] end
    5.96        | asts_of (Parser.Tip tok) =
    5.97            if Lexicon.valued_token tok
    5.98 @@ -185,9 +200,6 @@
    5.99            ((true, #1 (Term.dest_Const (ProofContext.read_const_proper ctxt false a)))
   5.100              handle ERROR _ => (false, Consts.intern (ProofContext.consts_of ctxt) a));
   5.101          val get_free = ProofContext.intern_skolem ctxt;
   5.102 -        fun markup_var xi = [Markup.name (Term.string_of_vname xi) Markup.var];
   5.103 -        fun markup_bound def id =
   5.104 -          [Markup.properties [(if def then Markup.defN else Markup.refN, id)] Markup.bound];
   5.105  
   5.106          val decodeT = typ_of_term (ProofContext.get_sort ctxt (term_sorts tm));
   5.107  
   5.108 @@ -390,7 +402,8 @@
   5.109  
   5.110      fun constify (ast as Ast.Constant _) = ast
   5.111        | constify (ast as Ast.Variable x) =
   5.112 -          if Syntax.is_const syn x orelse Long_Name.is_qualified x then Ast.Constant x
   5.113 +          if is_some (Syntax.lookup_const syn x) orelse Long_Name.is_qualified x
   5.114 +          then Ast.Constant x
   5.115            else ast
   5.116        | constify (Ast.Appl asts) = Ast.Appl (map constify asts);
   5.117  
   5.118 @@ -626,7 +639,7 @@
   5.119      val syn = ProofContext.syn_of ctxt;
   5.120      val idents = Local_Syntax.idents_of (ProofContext.syntax_of ctxt);
   5.121    in
   5.122 -    unparse_t (term_to_ast idents (Syntax.is_const syn))
   5.123 +    unparse_t (term_to_ast idents (is_some o Syntax.lookup_const syn))
   5.124        (Printer.pretty_term_ast (not (Pure_Thy.old_appl_syntax thy)))
   5.125        Markup.term ctxt
   5.126    end;