src/Pure/Syntax/lexicon.ML
changeset 62663 bea354f6ff21
parent 62529 8b7bdfc09f3b
child 62751 24e2b098bf44
equal deleted inserted replaced
62662:291cc01f56f5 62663:bea354f6ff21
    64     case_fixed: string -> 'a,
    64     case_fixed: string -> 'a,
    65     case_default: string -> 'a} -> string -> 'a
    65     case_default: string -> 'a} -> string -> 'a
    66   val is_marked: string -> bool
    66   val is_marked: string -> bool
    67   val dummy_type: term
    67   val dummy_type: term
    68   val fun_type: term
    68   val fun_type: term
    69   val pp_lexicon: Scan.lexicon -> Pretty.T
       
    70 end;
    69 end;
    71 
    70 
    72 structure Lexicon: LEXICON =
    71 structure Lexicon: LEXICON =
    73 struct
    72 struct
    74 
    73 
   453 val fun_type = Syntax.const (mark_type "fun");
   452 val fun_type = Syntax.const (mark_type "fun");
   454 
   453 
   455 
   454 
   456 (* toplevel pretty printing *)
   455 (* toplevel pretty printing *)
   457 
   456 
   458 val pp_lexicon =
   457 val _ =
   459   Pretty.str_list "{" "}" o map quote o Scan.dest_lexicon;
   458   PolyML.addPrettyPrinter (fn _ => fn _ =>
   460 
   459     Pretty.to_polyml o Pretty.str_list "{" "}" o map quote o Scan.dest_lexicon);
   461 end;
   460 
       
   461 end;