@{make_string} is available during Pure bootstrap;
authorwenzelm
Thu Mar 17 16:56:44 2016 +0100 (2016-03-17)
changeset 62662291cc01f56f5
parent 62661 c23ff2f45a18
child 62663 bea354f6ff21
@{make_string} is available during Pure bootstrap;
NEWS
src/Pure/ML/ml_antiquotation.ML
src/Pure/ML/ml_antiquotations.ML
src/Pure/ML/ml_compiler0.ML
src/Pure/ML/ml_pretty.ML
src/Pure/ROOT.ML
     1.1 --- a/NEWS	Thu Mar 17 13:44:18 2016 +0100
     1.2 +++ b/NEWS	Thu Mar 17 16:56:44 2016 +0100
     1.3 @@ -216,6 +216,9 @@
     1.4  
     1.5  *** ML ***
     1.6  
     1.7 +* Antiquotation @{make_string} is available during Pure bootstrap --
     1.8 +with approximative output quality.
     1.9 +
    1.10  * Option ML_exception_debugger controls detailed exception trace via the
    1.11  Poly/ML debugger. Relevant ML modules need to be compiled beforehand
    1.12  with ML_file_debug, or with ML_file and option ML_debugger enabled. Note
     2.1 --- a/src/Pure/ML/ml_antiquotation.ML	Thu Mar 17 13:44:18 2016 +0100
     2.2 +++ b/src/Pure/ML/ml_antiquotation.ML	Thu Mar 17 16:56:44 2016 +0100
     2.3 @@ -38,8 +38,10 @@
     2.4      (fn src => fn () =>
     2.5        ML_Context.value_decl "position" (ML_Syntax.print_position (#2 (Token.name_of_src src)))) #>
     2.6  
     2.7 +  inline (Binding.make ("make_string", @{here}))
     2.8 +    (Args.context >> (ML_Pretty.make_string_fn o ML_Context.struct_name)) #>
     2.9 +
    2.10    value (Binding.make ("binding", @{here}))
    2.11      (Scan.lift (Parse.position Args.name) >> ML_Syntax.make_binding));
    2.12  
    2.13  end;
    2.14 -
     3.1 --- a/src/Pure/ML/ml_antiquotations.ML	Thu Mar 17 13:44:18 2016 +0100
     3.2 +++ b/src/Pure/ML/ml_antiquotations.ML	Thu Mar 17 16:56:44 2016 +0100
     3.3 @@ -21,9 +21,6 @@
     3.4    ML_Antiquotation.inline @{binding assert}
     3.5      (Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")") #>
     3.6  
     3.7 -  ML_Antiquotation.inline @{binding make_string}
     3.8 -    (Args.context >> (ml_make_string o ML_Context.struct_name)) #>
     3.9 -
    3.10    ML_Antiquotation.declaration @{binding print}
    3.11      (Scan.lift (Scan.optional Args.name "Output.writeln"))
    3.12        (fn src => fn output => fn ctxt =>
    3.13 @@ -36,7 +33,8 @@
    3.14              \  (" ^ output ^ ") o (fn s => s ^ Position.here (" ^
    3.15              ML_Syntax.print_position pos ^ "));\n";
    3.16            val body =
    3.17 -            "(fn x => (" ^ struct_name ^ "." ^ a ^ " (" ^ ml_make_string struct_name ^ " x); x))";
    3.18 +            "(fn x => (" ^ struct_name ^ "." ^ a ^
    3.19 +              " (" ^ ML_Pretty.make_string_fn struct_name ^ " x); x))";
    3.20          in (K (env, body), ctxt') end));
    3.21  
    3.22  
     4.1 --- a/src/Pure/ML/ml_compiler0.ML	Thu Mar 17 13:44:18 2016 +0100
     4.2 +++ b/src/Pure/ML/ml_compiler0.ML	Thu Mar 17 16:56:44 2016 +0100
     4.3 @@ -33,14 +33,17 @@
     4.4  
     4.5  fun ml_input start_line name txt =
     4.6    let
     4.7 -    fun positions line (#"@" :: #"{" :: #"h" :: #"e" :: #"r" :: #"e" :: #"}" :: cs) res =
     4.8 +    fun input line (#"@" :: #"{" :: #"h" :: #"e" :: #"r" :: #"e" :: #"}" :: cs) res =
     4.9            let val s = "(Position.line_file_only " ^ Int.toString line ^ " \"" ^ name ^ "\")"
    4.10 -          in positions line cs (s :: res) end
    4.11 -      | positions line (#"\\" :: #"<" :: cs) res = positions line cs ("\\\\<" :: res)
    4.12 -      | positions line (#"\n" :: cs) res = positions (line + 1) cs ("\n" :: res)
    4.13 -      | positions line (c :: cs) res = positions line cs (str c :: res)
    4.14 -      | positions _ [] res = rev res;
    4.15 -  in String.concat (positions start_line (String.explode txt) []) end;
    4.16 +          in input line cs (s :: res) end
    4.17 +      | input line (#"@" :: #"{" :: #"m" :: #"a" :: #"k" :: #"e" :: #"_" ::
    4.18 +            #"s" :: #"t" :: #"r" :: #"i" :: #"n" :: #"g" :: #"}" :: cs) res =
    4.19 +          input line cs (ML_Pretty.make_string_fn "" :: res)
    4.20 +      | input line (#"\\" :: #"<" :: cs) res = input line cs ("\\\\<" :: res)
    4.21 +      | input line (#"\n" :: cs) res = input (line + 1) cs ("\n" :: res)
    4.22 +      | input line (c :: cs) res = input line cs (str c :: res)
    4.23 +      | input _ [] res = rev res;
    4.24 +  in String.concat (input start_line (String.explode txt) []) end;
    4.25  
    4.26  fun use_text ({name_space, here, print, error, ...}: context) {line, file, verbose, debug} text =
    4.27    let
     5.1 --- a/src/Pure/ML/ml_pretty.ML	Thu Mar 17 13:44:18 2016 +0100
     5.2 +++ b/src/Pure/ML/ml_pretty.ML	Thu Mar 17 16:56:44 2016 +0100
     5.3 @@ -19,6 +19,9 @@
     5.4    val from_polyml: PolyML.pretty -> pretty
     5.5    val get_print_depth: unit -> int
     5.6    val print_depth: int -> unit
     5.7 +  val format_polyml: int -> PolyML.pretty -> string
     5.8 +  val format: int -> pretty -> string
     5.9 +  val make_string_fn: string -> string
    5.10  end;
    5.11  
    5.12  structure ML_Pretty: ML_PRETTY =
    5.13 @@ -96,4 +99,33 @@
    5.14    val _ = print_depth 10;
    5.15  end;
    5.16  
    5.17 +
    5.18 +(* format *)
    5.19 +
    5.20 +fun format_polyml margin prt =
    5.21 +  let
    5.22 +    val result = Unsynchronized.ref [];
    5.23 +    val () = PolyML.prettyPrint (fn s => result := s :: ! result, margin) prt
    5.24 +  in String.concat (List.rev (! result)) end;
    5.25 +
    5.26 +fun format margin = format_polyml margin o to_polyml;
    5.27 +
    5.28 +
    5.29 +(* make string *)
    5.30 +
    5.31 +local
    5.32 +  fun pretty_string_of s =
    5.33 +    "(fn x => Pretty.string_of (Pretty.from_ML (ML_Pretty.from_polyml (" ^ s ^ "))))";
    5.34 +  fun pretty_value depth = "PolyML.prettyRepresentation (x, FixedInt.fromInt (" ^ depth ^ "))";
    5.35 +in
    5.36 +
    5.37 +fun make_string_fn local_env =
    5.38 +  if local_env <> "" then
    5.39 +    pretty_string_of (pretty_value (local_env ^ ".ML_print_depth ()"))
    5.40 +  else if List.exists (fn (a, _) => a = "Pretty") (#allStruct ML_Name_Space.global ()) then
    5.41 +    pretty_string_of (pretty_value "ML_Pretty.get_print_depth ()")
    5.42 +  else "(fn x => ML_Pretty.format_polyml 78 (" ^ pretty_value "ML_Pretty.get_print_depth ()" ^ "))";
    5.43 +
    5.44  end;
    5.45 +
    5.46 +end;
     6.1 --- a/src/Pure/ROOT.ML	Thu Mar 17 13:44:18 2016 +0100
     6.2 +++ b/src/Pure/ROOT.ML	Thu Mar 17 16:56:44 2016 +0100
     6.3 @@ -69,10 +69,6 @@
     6.4  PolyML.Compiler.printInAlphabeticalOrder := false;
     6.5  PolyML.Compiler.maxInlineSize := 80;
     6.6  
     6.7 -fun ml_make_string struct_name =
     6.8 -  "(fn x => Pretty.string_of (Pretty.from_ML (ML_Pretty.from_polyml (PolyML.prettyRepresentation (x, FixedInt.fromInt (" ^
     6.9 -    struct_name ^ ".ML_print_depth ()))))))";
    6.10 -
    6.11  
    6.12  (* ML debugger *)
    6.13