src/Pure/ML/ml_syntax.ML
author wenzelm
Wed Dec 29 20:41:33 2010 +0100 (2010-12-29)
changeset 41415 23533273220a
parent 40626 d86540f6ea0d
child 41491 a2ad5b824051
permissions -rw-r--r--
tuned ML toplevel pp for type string: observe depth limit;
     1 (*  Title:      Pure/ML/ml_syntax.ML
     2     Author:     Makarius
     3 
     4 Basic ML syntax operations.
     5 *)
     6 
     7 signature ML_SYNTAX =
     8 sig
     9   val reserved_names: string list
    10   val reserved: Name.context
    11   val is_reserved: string -> bool
    12   val is_identifier: string -> bool
    13   val atomic: string -> string
    14   val print_int: int -> string
    15   val print_pair: ('a -> string) -> ('b -> string) -> 'a * 'b -> string
    16   val print_list: ('a -> string) -> 'a list -> string
    17   val print_option: ('a -> string) -> 'a option -> string
    18   val print_char: string -> string
    19   val print_string: string -> string
    20   val print_strings: string list -> string
    21   val print_properties: Properties.T -> string
    22   val print_position: Position.T -> string
    23   val make_binding: string * Position.T -> string
    24   val print_indexname: indexname -> string
    25   val print_class: class -> string
    26   val print_sort: sort -> string
    27   val print_typ: typ -> string
    28   val print_term: term -> string
    29   val pretty_string: int -> string -> Pretty.T
    30 end;
    31 
    32 structure ML_Syntax: ML_SYNTAX =
    33 struct
    34 
    35 (* reserved words *)
    36 
    37 val reserved_names = filter Syntax.is_ascii_identifier ML_Lex.keywords;
    38 val reserved = Name.make_context reserved_names;
    39 val is_reserved = Name.is_declared reserved;
    40 
    41 
    42 (* identifiers *)
    43 
    44 fun is_identifier name =
    45   not (is_reserved name) andalso Syntax.is_ascii_identifier name;
    46 
    47 
    48 (* literal output -- unformatted *)
    49 
    50 val atomic = enclose "(" ")";
    51 
    52 val print_int = Int.toString;
    53 
    54 fun print_pair f1 f2 (x, y) = "(" ^ f1 x ^ ", " ^ f2 y ^ ")";
    55 
    56 fun print_list f = enclose "[" "]" o commas o map f;
    57 
    58 fun print_option f NONE = "NONE"
    59   | print_option f (SOME x) = "SOME (" ^ f x ^ ")";
    60 
    61 fun print_char s =
    62   if not (Symbol.is_char s) then s
    63   else if s = "\"" then "\\\""
    64   else if s = "\\" then "\\\\"
    65   else if s = "\t" then "\\t"
    66   else if s = "\n" then "\\n"
    67   else if s = "\r" then "\\r"
    68   else
    69     let val c = ord s in
    70       if c < 32 then "\\^" ^ chr (c + ord "@")
    71       else if c < 127 then s
    72       else "\\" ^ string_of_int c
    73     end;
    74 
    75 val print_string = quote o implode o map print_char o Symbol.explode;
    76 val print_strings = print_list print_string;
    77 
    78 val print_properties = print_list (print_pair print_string print_string);
    79 fun print_position pos = "Position.of_properties " ^ print_properties (Position.properties_of pos);
    80 fun make_binding (name, pos) = "Binding.make " ^ print_pair print_string print_position (name, pos);
    81 
    82 val print_indexname = print_pair print_string print_int;
    83 
    84 val print_class = print_string;
    85 val print_sort = print_list print_class;
    86 
    87 fun print_typ (Type arg) = "Type " ^ print_pair print_string (print_list print_typ) arg
    88   | print_typ (TFree arg) = "TFree " ^ print_pair print_string print_sort arg
    89   | print_typ (TVar arg) = "TVar " ^ print_pair print_indexname print_sort arg;
    90 
    91 fun print_term (Const arg) = "Const " ^ print_pair print_string print_typ arg
    92   | print_term (Free arg) = "Free " ^ print_pair print_string print_typ arg
    93   | print_term (Var arg) = "Var " ^ print_pair print_indexname print_typ arg
    94   | print_term (Bound i) = "Bound " ^ print_int i
    95   | print_term (Abs (s, T, t)) =
    96       "Abs (" ^ print_string s ^ ", " ^ print_typ T ^ ", " ^ print_term t ^ ")"
    97   | print_term (t1 $ t2) = atomic (print_term t1) ^ " $ " ^ atomic (print_term t2);
    98 
    99 
   100 (* toplevel pretty printing *)
   101 
   102 fun pretty_string max_len str =
   103   let
   104     val body =
   105       maps (fn XML.Elem _ => ["<markup>"] | XML.Text s => Symbol.explode s) (YXML.parse_body str)
   106         handle Fail _ => Symbol.explode str;
   107     val body' =
   108       if length body <= max_len then body
   109       else take max_len body @ ["..."];
   110   in Pretty.str (quote (implode (map print_char body'))) end;
   111 
   112 end;