src/Pure/ML/ml_syntax.ML
author wenzelm
Sat, 16 Jul 2011 17:11:49 +0200
changeset 43845 d89353d17f54
parent 42290 b1f544c84040
child 50238 98d35a7368bd
permissions -rw-r--r--
added File.fold_pages for streaming of large files; prefer \f notation;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
24582
57599da58045 ML_Lex.keywords;
wenzelm
parents: 24574
diff changeset
     1
(*  Title:      Pure/ML/ml_syntax.ML
24574
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
     3
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
     4
Basic ML syntax operations.
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
     5
*)
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
     6
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
     7
signature ML_SYNTAX =
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
     8
sig
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
     9
  val reserved_names: string list
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    10
  val reserved: Name.context
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    11
  val is_reserved: string -> bool
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    12
  val is_identifier: string -> bool
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    13
  val atomic: string -> string
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    14
  val print_int: int -> string
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    15
  val print_pair: ('a -> string) -> ('b -> string) -> 'a * 'b -> string
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    16
  val print_list: ('a -> string) -> 'a list -> string
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    17
  val print_option: ('a -> string) -> 'a option -> string
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    18
  val print_char: string -> string
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    19
  val print_string: string -> string
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    20
  val print_strings: string list -> string
30230
a2094a8c1672 added print_properties, print_position (again);
wenzelm
parents: 29606
diff changeset
    21
  val print_properties: Properties.T -> string
a2094a8c1672 added print_properties, print_position (again);
wenzelm
parents: 29606
diff changeset
    22
  val print_position: Position.T -> string
30523
4007ea1ddac2 added make_binding;
wenzelm
parents: 30230
diff changeset
    23
  val make_binding: string * Position.T -> string
24574
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    24
  val print_indexname: indexname -> string
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    25
  val print_class: class -> string
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    26
  val print_sort: sort -> string
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    27
  val print_typ: typ -> string
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    28
  val print_term: term -> string
41415
23533273220a tuned ML toplevel pp for type string: observe depth limit;
wenzelm
parents: 40626
diff changeset
    29
  val pretty_string: int -> string -> Pretty.T
24574
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    30
end;
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    31
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    32
structure ML_Syntax: ML_SYNTAX =
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    33
struct
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    34
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    35
(* reserved words *)
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    36
42290
b1f544c84040 discontinued special treatment of structure Lexicon;
wenzelm
parents: 42047
diff changeset
    37
val reserved_names = filter Lexicon.is_ascii_identifier ML_Lex.keywords;
24574
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    38
val reserved = Name.make_context reserved_names;
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    39
val is_reserved = Name.is_declared reserved;
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    40
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    41
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    42
(* identifiers *)
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    43
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    44
fun is_identifier name =
42290
b1f544c84040 discontinued special treatment of structure Lexicon;
wenzelm
parents: 42047
diff changeset
    45
  not (is_reserved name) andalso Lexicon.is_ascii_identifier name;
24574
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    46
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    47
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    48
(* literal output -- unformatted *)
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    49
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    50
val atomic = enclose "(" ")";
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    51
41491
a2ad5b824051 eliminated Int.toString;
wenzelm
parents: 41415
diff changeset
    52
val print_int = string_of_int;
24574
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    53
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    54
fun print_pair f1 f2 (x, y) = "(" ^ f1 x ^ ", " ^ f2 y ^ ")";
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    55
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    56
fun print_list f = enclose "[" "]" o commas o map f;
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    57
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    58
fun print_option f NONE = "NONE"
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    59
  | print_option f (SOME x) = "SOME (" ^ f x ^ ")";
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    60
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    61
fun print_char s =
31543
5bef6c7cc819 allow Isabelle symbols within low-level ML source;
wenzelm
parents: 30523
diff changeset
    62
  if not (Symbol.is_char s) then s
24574
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    63
  else if s = "\"" then "\\\""
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    64
  else if s = "\\" then "\\\\"
39514
d9cf3f833318 ML_Syntax.print_char: more readable output of some well-known ASCII controls -- this is relevant for ML toplevel pp;
wenzelm
parents: 37535
diff changeset
    65
  else if s = "\t" then "\\t"
d9cf3f833318 ML_Syntax.print_char: more readable output of some well-known ASCII controls -- this is relevant for ML toplevel pp;
wenzelm
parents: 37535
diff changeset
    66
  else if s = "\n" then "\\n"
43845
d89353d17f54 added File.fold_pages for streaming of large files;
wenzelm
parents: 42290
diff changeset
    67
  else if s = "\f" then "\\f"
39514
d9cf3f833318 ML_Syntax.print_char: more readable output of some well-known ASCII controls -- this is relevant for ML toplevel pp;
wenzelm
parents: 37535
diff changeset
    68
  else if s = "\r" then "\\r"
24574
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    69
  else
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    70
    let val c = ord s in
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    71
      if c < 32 then "\\^" ^ chr (c + ord "@")
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    72
      else if c < 127 then s
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    73
      else "\\" ^ string_of_int c
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    74
    end;
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    75
31543
5bef6c7cc819 allow Isabelle symbols within low-level ML source;
wenzelm
parents: 30523
diff changeset
    76
val print_string = quote o implode o map print_char o Symbol.explode;
24574
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    77
val print_strings = print_list print_string;
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    78
30230
a2094a8c1672 added print_properties, print_position (again);
wenzelm
parents: 29606
diff changeset
    79
val print_properties = print_list (print_pair print_string print_string);
a2094a8c1672 added print_properties, print_position (again);
wenzelm
parents: 29606
diff changeset
    80
fun print_position pos = "Position.of_properties " ^ print_properties (Position.properties_of pos);
30523
4007ea1ddac2 added make_binding;
wenzelm
parents: 30230
diff changeset
    81
fun make_binding (name, pos) = "Binding.make " ^ print_pair print_string print_position (name, pos);
30230
a2094a8c1672 added print_properties, print_position (again);
wenzelm
parents: 29606
diff changeset
    82
24574
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    83
val print_indexname = print_pair print_string print_int;
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    84
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    85
val print_class = print_string;
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    86
val print_sort = print_list print_class;
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    87
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    88
fun print_typ (Type arg) = "Type " ^ print_pair print_string (print_list print_typ) arg
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    89
  | print_typ (TFree arg) = "TFree " ^ print_pair print_string print_sort arg
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    90
  | print_typ (TVar arg) = "TVar " ^ print_pair print_indexname print_sort arg;
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    91
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    92
fun print_term (Const arg) = "Const " ^ print_pair print_string print_typ arg
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    93
  | print_term (Free arg) = "Free " ^ print_pair print_string print_typ arg
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    94
  | print_term (Var arg) = "Var " ^ print_pair print_indexname print_typ arg
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    95
  | print_term (Bound i) = "Bound " ^ print_int i
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    96
  | print_term (Abs (s, T, t)) =
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    97
      "Abs (" ^ print_string s ^ ", " ^ print_typ T ^ ", " ^ print_term t ^ ")"
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    98
  | print_term (t1 $ t2) = atomic (print_term t1) ^ " $ " ^ atomic (print_term t2);
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    99
37535
75de61a479e3 ML pretty printing of type string according to (quasi-abstract) YXML markup and symbols (including UTF8);
wenzelm
parents: 31543
diff changeset
   100
75de61a479e3 ML pretty printing of type string according to (quasi-abstract) YXML markup and symbols (including UTF8);
wenzelm
parents: 31543
diff changeset
   101
(* toplevel pretty printing *)
75de61a479e3 ML pretty printing of type string according to (quasi-abstract) YXML markup and symbols (including UTF8);
wenzelm
parents: 31543
diff changeset
   102
41415
23533273220a tuned ML toplevel pp for type string: observe depth limit;
wenzelm
parents: 40626
diff changeset
   103
fun pretty_string max_len str =
37535
75de61a479e3 ML pretty printing of type string according to (quasi-abstract) YXML markup and symbols (including UTF8);
wenzelm
parents: 31543
diff changeset
   104
  let
41415
23533273220a tuned ML toplevel pp for type string: observe depth limit;
wenzelm
parents: 40626
diff changeset
   105
    val body =
23533273220a tuned ML toplevel pp for type string: observe depth limit;
wenzelm
parents: 40626
diff changeset
   106
      maps (fn XML.Elem _ => ["<markup>"] | XML.Text s => Symbol.explode s) (YXML.parse_body str)
23533273220a tuned ML toplevel pp for type string: observe depth limit;
wenzelm
parents: 40626
diff changeset
   107
        handle Fail _ => Symbol.explode str;
23533273220a tuned ML toplevel pp for type string: observe depth limit;
wenzelm
parents: 40626
diff changeset
   108
    val body' =
23533273220a tuned ML toplevel pp for type string: observe depth limit;
wenzelm
parents: 40626
diff changeset
   109
      if length body <= max_len then body
42047
a7a4e04b5386 pretty_string: proper handling of negative max_len;
wenzelm
parents: 41491
diff changeset
   110
      else take (Int.max (max_len, 0)) body @ ["..."];
41415
23533273220a tuned ML toplevel pp for type string: observe depth limit;
wenzelm
parents: 40626
diff changeset
   111
  in Pretty.str (quote (implode (map print_char body'))) end;
37535
75de61a479e3 ML pretty printing of type string according to (quasi-abstract) YXML markup and symbols (including UTF8);
wenzelm
parents: 31543
diff changeset
   112
24574
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
   113
end;