merged
authorwenzelm
Wed Dec 29 22:51:33 2010 +0100 (2010-12-29)
changeset 41419e228a2e5a026
parent 41418 b6dc60638be0
parent 41416 a2208d3e2bd6
child 41420 005e7f8d02a7
merged
     1.1 --- a/src/Pure/General/symbol_pos.ML	Wed Dec 29 21:52:44 2010 +0100
     1.2 +++ b/src/Pure/General/symbol_pos.ML	Wed Dec 29 22:51:33 2010 +0100
     1.3 @@ -174,9 +174,11 @@
     1.4    in (implode syms', range syms') end;
     1.5  
     1.6  fun explode (str, pos) =
     1.7 -  fold_map (fn s => fn p => ((s, p), (Position.advance s p)))
     1.8 -    (Symbol.explode str) (Position.reset_range pos)
     1.9 -  |> #1 |> filter_out (fn (s, _) => s = Symbol.DEL);
    1.10 +  let
    1.11 +    val (res, _) =
    1.12 +      fold (fn s => fn (res, p) => ((s, p) :: res, Position.advance s p))
    1.13 +        (Symbol.explode str) ([], Position.reset_range pos);
    1.14 +  in fold (fn (s, p) => if s = Symbol.DEL then I else cons (s, p)) res [] end;
    1.15  
    1.16  end;
    1.17  
     2.1 --- a/src/Pure/ML/install_pp_polyml-5.3.ML	Wed Dec 29 21:52:44 2010 +0100
     2.2 +++ b/src/Pure/ML/install_pp_polyml-5.3.ML	Wed Dec 29 22:51:33 2010 +0100
     2.3 @@ -4,6 +4,9 @@
     2.4  Extra toplevel pretty-printing for Poly/ML 5.3.0.
     2.5  *)
     2.6  
     2.7 +PolyML.addPrettyPrinter (fn depth => fn _ => fn str =>
     2.8 +  ml_pretty (Pretty.to_ML (ML_Syntax.pretty_string (depth * 100) str)));
     2.9 +
    2.10  PolyML.addPrettyPrinter (fn depth => fn pretty => fn var =>
    2.11    pretty (Synchronized.value var, depth));
    2.12  
     3.1 --- a/src/Pure/ML/ml_syntax.ML	Wed Dec 29 21:52:44 2010 +0100
     3.2 +++ b/src/Pure/ML/ml_syntax.ML	Wed Dec 29 22:51:33 2010 +0100
     3.3 @@ -26,7 +26,7 @@
     3.4    val print_sort: sort -> string
     3.5    val print_typ: typ -> string
     3.6    val print_term: term -> string
     3.7 -  val pretty_string: string -> Pretty.T
     3.8 +  val pretty_string: int -> string -> Pretty.T
     3.9  end;
    3.10  
    3.11  structure ML_Syntax: ML_SYNTAX =
    3.12 @@ -99,12 +99,14 @@
    3.13  
    3.14  (* toplevel pretty printing *)
    3.15  
    3.16 -fun pretty_string raw_str =
    3.17 +fun pretty_string max_len str =
    3.18    let
    3.19 -    val str =
    3.20 -      implode (map (fn XML.Elem _ => "<markup>" | XML.Text s => s) (YXML.parse_body raw_str))
    3.21 -        handle Fail _ => raw_str;
    3.22 -    val syms = Symbol.explode str;
    3.23 -  in Pretty.str (quote (implode (map print_char syms))) end;
    3.24 +    val body =
    3.25 +      maps (fn XML.Elem _ => ["<markup>"] | XML.Text s => Symbol.explode s) (YXML.parse_body str)
    3.26 +        handle Fail _ => Symbol.explode str;
    3.27 +    val body' =
    3.28 +      if length body <= max_len then body
    3.29 +      else take max_len body @ ["..."];
    3.30 +  in Pretty.str (quote (implode (map print_char body'))) end;
    3.31  
    3.32  end;
     4.1 --- a/src/Pure/pure_setup.ML	Wed Dec 29 21:52:44 2010 +0100
     4.2 +++ b/src/Pure/pure_setup.ML	Wed Dec 29 22:51:33 2010 +0100
     4.3 @@ -18,10 +18,6 @@
     4.4  
     4.5  (* ML toplevel pretty printing *)
     4.6  
     4.7 -if String.isPrefix "polyml" ml_system
     4.8 -then toplevel_pp ["String", "string"] "ML_Syntax.pretty_string"
     4.9 -else ();
    4.10 -
    4.11  toplevel_pp ["Pretty", "T"] "(fn _: Pretty.T => Pretty.str \"<pretty>\")";
    4.12  toplevel_pp ["Task_Queue", "task"] "Pretty.str o Task_Queue.str_of_task";
    4.13  toplevel_pp ["Task_Queue", "group"] "Pretty.str o Task_Queue.str_of_group";