tuned ML toplevel pp for type string: observe depth limit;
authorwenzelm
Wed Dec 29 20:41:33 2010 +0100 (2010-12-29)
changeset 4141523533273220a
parent 41414 00b2b6716ed8
child 41416 a2208d3e2bd6
tuned ML toplevel pp for type string: observe depth limit;
src/Pure/ML/install_pp_polyml-5.3.ML
src/Pure/ML/ml_syntax.ML
src/Pure/pure_setup.ML
     1.1 --- a/src/Pure/ML/install_pp_polyml-5.3.ML	Wed Dec 29 18:18:42 2010 +0100
     1.2 +++ b/src/Pure/ML/install_pp_polyml-5.3.ML	Wed Dec 29 20:41:33 2010 +0100
     1.3 @@ -4,6 +4,9 @@
     1.4  Extra toplevel pretty-printing for Poly/ML 5.3.0.
     1.5  *)
     1.6  
     1.7 +PolyML.addPrettyPrinter (fn depth => fn _ => fn str =>
     1.8 +  ml_pretty (Pretty.to_ML (ML_Syntax.pretty_string (depth * 100) str)));
     1.9 +
    1.10  PolyML.addPrettyPrinter (fn depth => fn pretty => fn var =>
    1.11    pretty (Synchronized.value var, depth));
    1.12  
     2.1 --- a/src/Pure/ML/ml_syntax.ML	Wed Dec 29 18:18:42 2010 +0100
     2.2 +++ b/src/Pure/ML/ml_syntax.ML	Wed Dec 29 20:41:33 2010 +0100
     2.3 @@ -26,7 +26,7 @@
     2.4    val print_sort: sort -> string
     2.5    val print_typ: typ -> string
     2.6    val print_term: term -> string
     2.7 -  val pretty_string: string -> Pretty.T
     2.8 +  val pretty_string: int -> string -> Pretty.T
     2.9  end;
    2.10  
    2.11  structure ML_Syntax: ML_SYNTAX =
    2.12 @@ -99,12 +99,14 @@
    2.13  
    2.14  (* toplevel pretty printing *)
    2.15  
    2.16 -fun pretty_string raw_str =
    2.17 +fun pretty_string max_len str =
    2.18    let
    2.19 -    val str =
    2.20 -      implode (map (fn XML.Elem _ => "<markup>" | XML.Text s => s) (YXML.parse_body raw_str))
    2.21 -        handle Fail _ => raw_str;
    2.22 -    val syms = Symbol.explode str;
    2.23 -  in Pretty.str (quote (implode (map print_char syms))) end;
    2.24 +    val body =
    2.25 +      maps (fn XML.Elem _ => ["<markup>"] | XML.Text s => Symbol.explode s) (YXML.parse_body str)
    2.26 +        handle Fail _ => Symbol.explode str;
    2.27 +    val body' =
    2.28 +      if length body <= max_len then body
    2.29 +      else take max_len body @ ["..."];
    2.30 +  in Pretty.str (quote (implode (map print_char body'))) end;
    2.31  
    2.32  end;
     3.1 --- a/src/Pure/pure_setup.ML	Wed Dec 29 18:18:42 2010 +0100
     3.2 +++ b/src/Pure/pure_setup.ML	Wed Dec 29 20:41:33 2010 +0100
     3.3 @@ -18,10 +18,6 @@
     3.4  
     3.5  (* ML toplevel pretty printing *)
     3.6  
     3.7 -if String.isPrefix "polyml" ml_system
     3.8 -then toplevel_pp ["String", "string"] "ML_Syntax.pretty_string"
     3.9 -else ();
    3.10 -
    3.11  toplevel_pp ["Pretty", "T"] "(fn _: Pretty.T => Pretty.str \"<pretty>\")";
    3.12  toplevel_pp ["Task_Queue", "task"] "Pretty.str o Task_Queue.str_of_task";
    3.13  toplevel_pp ["Task_Queue", "group"] "Pretty.str o Task_Queue.str_of_group";