diff --git a/src/HOL/Library/code_test.ML b/src/HOL/Library/code_test.ML
--- a/src/HOL/Library/code_test.ML
+++ b/src/HOL/Library/code_test.ML
@@ -1,566 +1,566 @@
 (*  Title:      HOL/Library/code_test.ML
     Author:     Andreas Lochbihler, ETH Zürich
 
 Test infrastructure for the code generator.
 *)
 
 signature CODE_TEST =
 sig
   val add_driver:
     string * ((Proof.context -> (string * string) list * string -> Path.T -> string) * string) ->
     theory -> theory
   val debug: bool Config.T
   val successN: string
   val failureN: string
   val start_markerN: string
   val end_markerN: string
   val test_terms: Proof.context -> term list -> string -> unit
   val test_code_cmd: string list -> string list -> Proof.context -> unit
   val eval_term: string -> Proof.context -> term -> term
   val check_settings: string -> string -> string -> unit
   val compile: string -> string -> unit
   val evaluate: string -> string -> string
   val evaluate_in_polyml: Proof.context -> (string * string) list * string -> Path.T -> string
   val evaluate_in_mlton: Proof.context -> (string * string) list * string -> Path.T -> string
   val evaluate_in_smlnj: Proof.context -> (string * string) list * string -> Path.T -> string
   val evaluate_in_ocaml: Proof.context -> (string * string) list * string -> Path.T -> string
   val ghc_options: string Config.T
   val evaluate_in_ghc: Proof.context -> (string * string) list * string -> Path.T -> string
   val evaluate_in_scala: Proof.context -> (string * string) list * string -> Path.T -> string
   val target_Scala: string
   val target_Haskell: string
 end
 
 structure Code_Test: CODE_TEST =
 struct
 
 (* convert a list of terms into nested tuples and back *)
 
 fun mk_tuples [] = \<^term>\<open>()\<close>
   | mk_tuples [t] = t
   | mk_tuples (t :: ts) = HOLogic.mk_prod (t, mk_tuples ts)
 
 fun dest_tuples (Const (\<^const_name>\<open>Pair\<close>, _) $ l $ r) = l :: dest_tuples r
   | dest_tuples t = [t]
 
 
 fun last_field sep str =
   let
     val n = size sep
     val len = size str
     fun find i =
       if i < 0 then NONE
       else if String.substring (str, i, n) = sep then SOME i
       else find (i - 1)
   in
     (case find (len - n) of
       NONE => NONE
     | SOME i => SOME (String.substring (str, 0, i), String.extract (str, i + n, NONE)))
   end
 
 fun split_first_last start stop s =
   (case first_field start s of
     NONE => NONE
   | SOME (initial, rest) =>
       (case last_field stop rest of
         NONE => NONE
       | SOME (middle, tail) => SOME (initial, middle, tail)))
 
 
 (* data slot for drivers *)
 
 structure Drivers = Theory_Data
 (
   type T =
     (string * ((Proof.context -> (string * string) list * string -> Path.T -> string) * string)) list
   val empty = []
   val extend = I
   fun merge data : T = AList.merge (op =) (K true) data
 )
 
 val add_driver = Drivers.map o AList.update (op =)
 val get_driver = AList.lookup (op =) o Drivers.get
 
 (*
   Test drivers must produce output of the following format:
 
   The start of the relevant data is marked with start_markerN,
   its end with end_markerN.
 
   Between these two markers, every line corresponds to one test.
   Lines of successful tests start with successN, failures start with failureN.
   The failure failureN may continue with the YXML encoding of the evaluated term.
   There must not be any additional whitespace in between.
 *)
 
 
 (* parsing of results *)
 
 val successN = "True"
 val failureN = "False"
 val start_markerN = "*@*Isabelle/Code_Test-start*@*"
 val end_markerN = "*@*Isabelle/Code_Test-end*@*"
 
 fun parse_line line =
   if String.isPrefix successN line then (true, NONE)
   else if String.isPrefix failureN line then (false,
     if size line > size failureN then
       String.extract (line, size failureN, NONE)
       |> YXML.parse_body
       |> Term_XML.Decode.term_raw
       |> dest_tuples
       |> SOME
     else NONE)
   else raise Fail ("Cannot parse result of evaluation:\n" ^ line)
 
 fun parse_result target out =
   (case split_first_last start_markerN end_markerN out of
     NONE => error ("Evaluation failed for " ^ target ^ "!\nCompiler output:\n" ^ out)
   | SOME (_, middle, _) => middle |> trim_split_lines |> map parse_line)
 
 
 (* pretty printing of test results *)
 
 fun pretty_eval _ NONE _ = []
   | pretty_eval ctxt (SOME evals) ts =
       [Pretty.fbrk,
        Pretty.big_list "Evaluated terms"
          (map (fn (t, eval) => Pretty.block
            [Syntax.pretty_term ctxt t, Pretty.brk 1, Pretty.str "=", Pretty.brk 1,
             Syntax.pretty_term ctxt eval])
          (ts ~~ evals))]
 
 fun pretty_failure ctxt target (((_, evals), query), eval_ts) =
   Pretty.block (Pretty.text ("Test in " ^ target ^ " failed for") @
     [Pretty.brk 1, Pretty.quote (Syntax.pretty_term ctxt query)] @
     pretty_eval ctxt evals eval_ts)
 
 fun pretty_failures ctxt target failures =
   Pretty.blk (0, Pretty.fbreaks (map (pretty_failure ctxt target) failures))
 
 
 (* driver invocation *)
 
 val debug = Attrib.setup_config_bool \<^binding>\<open>code_test_debug\<close> (K false)
 
 fun with_debug_dir name f =
   let
     val dir =
       Path.append (Path.explode "$ISABELLE_HOME_USER") (Path.basic (name ^ serial_string ()))
     val _ = Isabelle_System.mkdirs dir
   in Exn.release (Exn.capture f dir) end
 
 fun dynamic_value_strict ctxt t compiler =
   let
     val thy = Proof_Context.theory_of ctxt
     val (driver, target) =
       (case get_driver thy compiler of
         NONE => error ("No driver for target " ^ compiler)
       | SOME drv => drv)
     val with_dir = if Config.get ctxt debug then with_debug_dir else Isabelle_System.with_tmp_dir
     fun eval result =
       with_dir "Code_Test" (driver ctxt ((apfst o map o apfst) Long_Name.implode result))
       |> parse_result compiler
     fun evaluator program _ vs_ty deps =
       Exn.interruptible_capture eval
         (Code_Target.compilation_text ctxt target program deps true vs_ty)
     fun postproc f = map (apsnd (Option.map (map f)))
   in Exn.release (Code_Thingol.dynamic_value ctxt (Exn.map_res o postproc) evaluator t) end
 
 
 (* term preprocessing *)
 
 fun add_eval (Const (\<^const_name>\<open>Trueprop\<close>, _) $ t) = add_eval t
   | add_eval (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ lhs $ rhs) = (fn acc =>
       acc
       |> add_eval rhs
       |> add_eval lhs
       |> cons rhs
       |> cons lhs)
   | add_eval (Const (\<^const_name>\<open>Not\<close>, _) $ t) = add_eval t
   | add_eval (Const (\<^const_name>\<open>Orderings.ord_class.less_eq\<close>, _) $ lhs $ rhs) = (fn acc =>
       lhs :: rhs :: acc)
   | add_eval (Const (\<^const_name>\<open>Orderings.ord_class.less\<close>, _) $ lhs $ rhs) = (fn acc =>
       lhs :: rhs :: acc)
   | add_eval _ = I
 
 fun mk_term_of [] = \<^term>\<open>None :: (unit \<Rightarrow> yxml_of_term) option\<close>
   | mk_term_of ts =
       let
         val tuple = mk_tuples ts
         val T = fastype_of tuple
       in
         \<^term>\<open>Some :: (unit \<Rightarrow> yxml_of_term) \<Rightarrow> (unit \<Rightarrow> yxml_of_term) option\<close> $
           (absdummy \<^typ>\<open>unit\<close> (\<^const>\<open>yxml_string_of_term\<close> $
             (Const (\<^const_name>\<open>Code_Evaluation.term_of\<close>, T --> \<^typ>\<open>term\<close>) $ tuple)))
       end
 
 fun test_terms ctxt ts target =
   let
     val thy = Proof_Context.theory_of ctxt
 
     fun term_of t = Sign.of_sort thy (fastype_of t, \<^sort>\<open>term_of\<close>)
 
     fun ensure_bool t =
       (case fastype_of t of
         \<^typ>\<open>bool\<close> => ()
       | _ =>
         error (Pretty.string_of
           (Pretty.block [Pretty.str "Test case not of type bool:", Pretty.brk 1,
             Syntax.pretty_term ctxt t])))
 
     val _ = List.app ensure_bool ts
 
     val evals = map (fn t => filter term_of (add_eval t [])) ts
     val eval = map mk_term_of evals
 
     val t =
       HOLogic.mk_list \<^typ>\<open>bool \<times> (unit \<Rightarrow> yxml_of_term) option\<close>
         (map HOLogic.mk_prod (ts ~~ eval))
 
     val result = dynamic_value_strict ctxt t target
 
     val failed =
       filter_out (fst o fst o fst) (result ~~ ts ~~ evals)
       handle ListPair.UnequalLengths =>
         error ("Evaluation failed!\nWrong number of test results: " ^ string_of_int (length result))
   in
     (case failed of
       [] => ()
     | _ => error (Pretty.string_of (pretty_failures ctxt target failed)))
   end
 
 fun test_code_cmd raw_ts targets ctxt =
   let
     val ts = Syntax.read_terms ctxt raw_ts
     val frees = fold Term.add_frees ts []
     val _ =
       if null frees then ()
       else error (Pretty.string_of
         (Pretty.block (Pretty.str "Terms contain free variables:" :: Pretty.brk 1 ::
           Pretty.commas (map (Syntax.pretty_term ctxt o Free) frees))))
   in List.app (test_terms ctxt ts) targets end
 
 fun eval_term target ctxt t =
   let
     val frees = Term.add_frees t []
     val _ =
       if null frees then ()
       else
         error (Pretty.string_of
           (Pretty.block (Pretty.str "Term contains free variables:" :: Pretty.brk 1 ::
             Pretty.commas (map (Syntax.pretty_term ctxt o Free) frees))))
 
     val T = fastype_of t
     val _ =
       if Sign.of_sort (Proof_Context.theory_of ctxt) (T, \<^sort>\<open>term_of\<close>) then ()
       else error ("Type " ^ Syntax.string_of_typ ctxt T ^
        " of term not of sort " ^ Syntax.string_of_sort ctxt \<^sort>\<open>term_of\<close>)
 
     val t' =
       HOLogic.mk_list \<^typ>\<open>bool \<times> (unit \<Rightarrow> yxml_of_term) option\<close>
         [HOLogic.mk_prod (\<^term>\<open>False\<close>, mk_term_of [t])]
 
     val result = dynamic_value_strict ctxt t' target
   in (case result of [(_, SOME [t])] => t | _ => error "Evaluation failed") end
 
 
 (* check and invoke compiler *)
 
 fun check_settings compiler var descr =
   if getenv var = "" then
     error (Pretty.string_of (Pretty.para
       ("Environment variable " ^ var ^ " is not set. To test code generation with " ^
         compiler ^ ", set this variable to your " ^ descr ^
         " in the $ISABELLE_HOME_USER/etc/settings file.")))
   else ();
 
 fun compile compiler cmd =
   let val (out, ret) = Isabelle_System.bash_output cmd in
     if ret = 0 then ()
     else error ("Compilation with " ^ compiler ^ " failed:\n" ^ cmd ^ "\n" ^ out)
   end
 
 fun evaluate compiler cmd =
   let val (out, res) = Isabelle_System.bash_output cmd in
     if res = 0 then out
     else error ("Evaluation for " ^ compiler ^ " terminated with error code " ^
       string_of_int res ^ "\nCompiler output:\n" ^ out)
   end
 
 
 (* driver for PolyML *)
 
 val polymlN = "PolyML"
 
 fun evaluate_in_polyml ctxt (code_files, value_name) dir =
   let
     val code = #2 (the_single code_files);
     val code_path = Path.append dir (Path.basic "generated.sml")
     val driver_path = Path.append dir (Path.basic "driver.sml")
     val out_path = Path.append dir (Path.basic "out")
     val string = ML_Syntax.print_string
     val driver = \<^verbatim>\<open>
 fun main prog_name =
   let
     fun format (true, _) = \<close> ^ string successN ^ \<^verbatim>\<open> ^ "\n"
       | format (false, NONE) = \<close> ^ string failureN ^ \<^verbatim>\<open> ^ "\n"
       | format (false, SOME t) = \<close> ^ string failureN ^ \<^verbatim>\<open> ^ t () ^ "\n"
     val result = \<close> ^ value_name ^ \<^verbatim>\<open> ()
     val result_text = \<close> ^
       string start_markerN ^
       \<^verbatim>\<open> ^ String.concat (map format result) ^ \<close> ^
       string end_markerN ^ \<^verbatim>\<open>
-    val out = BinIO.openOut \<close> ^ string (Path.implode (Path.expand out_path)) ^ \<^verbatim>\<open>
+    val out = BinIO.openOut \<close> ^ ML_Syntax.print_platform_path out_path ^ \<^verbatim>\<open>
     val _ = BinIO.output (out, Byte.stringToBytes result_text)
     val _ = BinIO.closeOut out
   in () end;
 \<close>
   in
     if Config.get ctxt debug
     then (File.write code_path code; File.write driver_path driver)
     else ();
 
     ML_Context.eval
       {environment = ML_Env.SML, redirect = false, verbose = false, debug = NONE,
         writeln = writeln, warning = warning}
       Position.none
       (ML_Lex.read_text (code, Path.position code_path) @
        ML_Lex.read_text (driver, Path.position driver_path) @
        ML_Lex.read "main ()");
 
     File.read out_path
   end
 
 
 (* driver for mlton *)
 
 val mltonN = "MLton"
 val ISABELLE_MLTON = "ISABELLE_MLTON"
 
 fun evaluate_in_mlton (_: Proof.context) (code_files, value_name) dir =
   let
     val compiler = mltonN
     val generatedN = "generated.sml"
     val driverN = "driver.sml"
     val projectN = "test"
 
     val code_path = Path.append dir (Path.basic generatedN)
     val driver_path = Path.append dir (Path.basic driverN)
     val basis_path = Path.append dir (Path.basic (projectN ^ ".mlb"))
     val driver =
       "fun format_term NONE = \"\"\n" ^
       "  | format_term (SOME t) = t ();\n" ^
       "fun format (true, _) = \"" ^ successN ^ "\\n\"\n" ^
       "  | format (false, to) = \"" ^ failureN ^ "\" ^ format_term to ^ \"\\n\";\n" ^
       "val result = " ^ value_name ^ " ();\n" ^
       "val _ = print \"" ^ start_markerN ^ "\";\n" ^
       "val _ = map (print o format) result;\n" ^
       "val _ = print \"" ^ end_markerN ^ "\";\n"
     val cmd = "\"$ISABELLE_MLTON\" -default-type intinf " ^ File.bash_path basis_path
   in
     check_settings compiler ISABELLE_MLTON "MLton executable";
     List.app (File.write code_path o snd) code_files;
     File.write driver_path driver;
     File.write basis_path ("$(SML_LIB)/basis/basis.mlb\n" ^ generatedN ^ "\n" ^ driverN);
     compile compiler cmd;
     evaluate compiler (File.bash_path (Path.append dir (Path.basic projectN)))
   end
 
 
 (* driver for SML/NJ *)
 
 val smlnjN = "SMLNJ"
 val ISABELLE_SMLNJ = "ISABELLE_SMLNJ"
 
 fun evaluate_in_smlnj (_: Proof.context) (code_files, value_name) dir =
   let
     val compiler = smlnjN
     val generatedN = "generated.sml"
     val driverN = "driver.sml"
 
     val code_path = Path.append dir (Path.basic generatedN)
     val driver_path = Path.append dir (Path.basic driverN)
     val driver =
       "structure Test = struct\n" ^
       "fun main prog_name =\n" ^
       "  let\n" ^
       "    fun format_term NONE = \"\"\n" ^
       "      | format_term (SOME t) = t ();\n" ^
       "    fun format (true, _) = \"" ^ successN ^ "\\n\"\n" ^
       "      | format (false, to) = \"" ^ failureN ^ "\" ^ format_term to ^ \"\\n\";\n" ^
       "    val result = " ^ value_name ^ " ();\n" ^
       "    val _ = print \"" ^ start_markerN ^ "\";\n" ^
       "    val _ = map (print o format) result;\n" ^
       "    val _ = print \"" ^ end_markerN ^ "\";\n" ^
       "  in\n" ^
       "    0\n" ^
       "  end;\n" ^
       "end;"
     val ml_source =
       "Control.MC.matchRedundantError := false; Control.MC.matchRedundantWarn := false;" ^
       "use " ^ ML_Syntax.print_string (File.platform_path code_path) ^
       "; use " ^ ML_Syntax.print_string (File.platform_path driver_path) ^
       "; Test.main ();"
   in
     check_settings compiler ISABELLE_SMLNJ "SMLNJ executable";
     List.app (File.write code_path o snd) code_files;
     File.write driver_path driver;
     evaluate compiler ("echo " ^ Bash.string ml_source ^ " | \"$ISABELLE_SMLNJ\"")
   end
 
 
 (* driver for OCaml *)
 
 val ocamlN = "OCaml"
 val ISABELLE_OCAMLFIND = "ISABELLE_OCAMLFIND"
 
 fun evaluate_in_ocaml (_: Proof.context) (code_files, value_name) dir =
   let
     val compiler = ocamlN
 
     val code_path = Path.append dir (Path.basic "generated.ml")
     val driver_path = Path.append dir (Path.basic "driver.ml")
     val driver =
       "let format_term = function\n" ^
       "  | None -> \"\"\n" ^
       "  | Some t -> t ();;\n" ^
       "let format = function\n" ^
       "  | (true, _) -> \"" ^ successN ^ "\\n\"\n" ^
       "  | (false, x) -> \"" ^ failureN ^ "\" ^ format_term x ^ \"\\n\";;\n" ^
       "let result = " ^ ("Generated." ^ value_name) ^ " ();;\n" ^
       "let main x =\n" ^
       "  let _ = print_string \"" ^ start_markerN ^ "\" in\n" ^
       "  let _ = List.map (fun x -> print_string (format x)) result in\n" ^
       "  print_string \"" ^ end_markerN ^ "\";;\n" ^
       "main ();;"
     val compiled_path = Path.append dir (Path.basic "test")
     val cmd =
       "\"$ISABELLE_OCAMLFIND\" ocamlopt -w pu -package zarith -linkpkg" ^
       " -o " ^ File.bash_path compiled_path ^ " -I " ^ File.bash_path dir ^ " " ^
       File.bash_path code_path ^ " " ^ File.bash_path driver_path ^ " </dev/null"
   in
     check_settings compiler ISABELLE_OCAMLFIND "ocamlfind executable";
     List.app (File.write code_path o snd) code_files;
     File.write driver_path driver;
     compile compiler cmd;
     evaluate compiler (File.bash_path compiled_path)
   end
 
 
 (* driver for GHC *)
 
 val ghcN = "GHC"
 val ISABELLE_GHC = "ISABELLE_GHC"
 
 val ghc_options = Attrib.setup_config_string \<^binding>\<open>code_test_ghc\<close> (K "")
 
 fun evaluate_in_ghc ctxt (code_files, value_name) dir =
   let
     val compiler = ghcN
     val modules = map fst code_files
 
     val driver_path = Path.append dir (Path.basic "Main.hs")
     val driver =
       "module Main where {\n" ^
       implode (map (fn module => "import qualified " ^ unsuffix ".hs" module ^ ";\n") modules) ^
       "main = do {\n" ^
       "    let {\n" ^
       "      format_term Nothing = \"\";\n" ^
       "      format_term (Just t) = t ();\n" ^
       "      format (True, _) = \"" ^ successN ^ "\\n\";\n" ^
       "      format (False, to) = \"" ^ failureN ^ "\" ++ format_term to ++ \"\\n\";\n" ^
       "      result = " ^ value_name ^ " ();\n" ^
       "    };\n" ^
       "    Prelude.putStr \"" ^ start_markerN ^ "\";\n" ^
       "    Prelude.mapM_ (putStr . format) result;\n" ^
       "    Prelude.putStr \"" ^ end_markerN ^ "\";\n" ^
       "  }\n" ^
       "}\n"
 
     val compiled_path = Path.append dir (Path.basic "test")
     val cmd =
       "\"$ISABELLE_GHC\" " ^ Code_Haskell.language_params ^ " " ^
       Config.get ctxt ghc_options ^ " -o " ^
       File.bash_platform_path compiled_path ^ " " ^
       File.bash_platform_path driver_path ^ " -i" ^
       File.bash_platform_path dir
   in
     check_settings compiler ISABELLE_GHC "GHC executable";
     List.app (fn (name, code) => File.write (Path.append dir (Path.basic name)) code) code_files;
     File.write driver_path driver;
     compile compiler cmd;
     evaluate compiler (File.bash_path compiled_path)
   end
 
 
 (* driver for Scala *)
 
 val scalaN = "Scala"
 
 fun evaluate_in_scala (_: Proof.context) (code_files, value_name) dir =
   let
     val compiler = scalaN
     val generatedN = "Generated_Code"
     val driverN = "Driver.scala"
 
     val code_path = Path.append dir (Path.basic (generatedN ^ ".scala"))
     val driver_path = Path.append dir (Path.basic driverN)
     val driver =
       "import " ^ generatedN ^ "._\n" ^
       "object Test {\n" ^
       "  def format_term(x : Option[Unit => String]) : String = x match {\n" ^
       "    case None => \"\"\n" ^
       "    case Some(x) => x(())\n" ^
       "  }\n" ^
       "  def format(term : (Boolean, Option[Unit => String])) : String = term match {\n" ^
       "      case (true, _) => \"True\\n\"\n" ^
       "      case (false, x) => \"False\" + format_term(x) + \"\\n\"\n" ^
       "  }\n" ^
       "  def main(args:Array[String]) = {\n" ^
       "    val result = " ^ value_name ^ "(());\n" ^
       "    print(\"" ^ start_markerN ^ "\");\n" ^
       "    result.map{test:(Boolean, Option[Unit => String]) => print(format(test))};\n" ^
       "    print(\"" ^ end_markerN ^ "\");\n" ^
       "  }\n" ^
       "}\n"
     val compile_cmd =
       "isabelle_scala scalac $ISABELLE_SCALAC_OPTIONS -d " ^ File.bash_platform_path dir ^
       " -classpath " ^ File.bash_platform_path dir ^ " " ^
       File.bash_platform_path code_path ^ " " ^ File.bash_platform_path driver_path
     val run_cmd = "isabelle_scala scala -cp " ^ File.bash_platform_path dir ^ " Test"
   in
     List.app (File.write code_path o snd) code_files;
     File.write driver_path driver;
     compile compiler compile_cmd;
     evaluate compiler run_cmd
   end
 
 
 (* command setup *)
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>test_code\<close>
     "compile test cases to target languages, execute them and report results"
       (Scan.repeat1 Parse.prop -- (\<^keyword>\<open>in\<close> |-- Scan.repeat1 Parse.name)
         >> (fn (ts, targets) => Toplevel.keep (test_code_cmd ts targets o Toplevel.context_of)))
 
 val target_Scala = "Scala_eval"
 val target_Haskell = "Haskell_eval"
 
 val _ = Theory.setup
    (Code_Target.add_derived_target (target_Scala, [(Code_Scala.target, I)])
     #> Code_Target.add_derived_target (target_Haskell, [(Code_Haskell.target, I)]))
 
 val _ =
   Theory.setup (fold add_driver
     [(polymlN, (evaluate_in_polyml, Code_ML.target_SML)),
      (mltonN, (evaluate_in_mlton, Code_ML.target_SML)),
      (smlnjN, (evaluate_in_smlnj, Code_ML.target_SML)),
      (ocamlN, (evaluate_in_ocaml, Code_ML.target_OCaml)),
      (ghcN, (evaluate_in_ghc, target_Haskell)),
      (scalaN, (evaluate_in_scala, target_Scala))]
   #> fold (fn target => Value_Command.add_evaluator (Binding.name target, eval_term target) #> snd)
       [polymlN, mltonN, smlnjN, ocamlN, ghcN, scalaN])
 
 end
diff --git a/src/Pure/ML/ml_syntax.ML b/src/Pure/ML/ml_syntax.ML
--- a/src/Pure/ML/ml_syntax.ML
+++ b/src/Pure/ML/ml_syntax.ML
@@ -1,143 +1,146 @@
 (*  Title:      Pure/ML/ml_syntax.ML
     Author:     Makarius
 
 Concrete ML syntax for basic values.
 *)
 
 signature ML_SYNTAX =
 sig
   val reserved_names: string list
   val reserved: Name.context
   val is_reserved: string -> bool
   val is_identifier: string -> bool
   val atomic: string -> string
   val print_int: int -> string
   val print_pair: ('a -> string) -> ('b -> string) -> 'a * 'b -> string
   val print_list: ('a -> string) -> 'a list -> string
   val print_option: ('a -> string) -> 'a option -> string
   val print_symbol_char: Symbol.symbol -> string
   val print_symbol: Symbol.symbol -> string
   val print_string: string -> string
   val print_strings: string list -> string
   val print_path: Path.T -> string
+  val print_platform_path: Path.T -> string
   val print_properties: Properties.T -> string
   val print_position: Position.T -> string
   val print_range: Position.range -> string
   val print_path_binding: Path.binding -> string
   val make_binding: string * Position.T -> string
   val print_indexname: indexname -> string
   val print_class: class -> string
   val print_sort: sort -> string
   val print_typ: typ -> string
   val print_term: term -> string
   val pretty_string: int -> string -> Pretty.T
 end;
 
 structure ML_Syntax: ML_SYNTAX =
 struct
 
 (* reserved words *)
 
 val reserved_names = filter Symbol.is_ascii_identifier ML_Lex.keywords;
 val reserved = Name.make_context reserved_names;
 val is_reserved = Name.is_declared reserved;
 
 
 (* identifiers *)
 
 fun is_identifier name =
   not (is_reserved name) andalso Symbol.is_ascii_identifier name;
 
 
 (* literal output -- unformatted *)
 
 val atomic = enclose "(" ")";
 
 val print_int = string_of_int;
 
 fun print_pair f1 f2 (x, y) = "(" ^ f1 x ^ ", " ^ f2 y ^ ")";
 
 fun print_list f = enclose "[" "]" o commas o map f;
 
 fun print_option f NONE = "NONE"
   | print_option f (SOME x) = "SOME (" ^ f x ^ ")";
 
 fun print_symbol_char s =
   if Symbol.is_char s then
     (case ord s of
       34 => "\\\""
     | 92 => "\\\\"
     | 7 => "\\a"
     | 8 => "\\b"
     | 9 => "\\t"
     | 10 => "\\n"
     | 11 => "\\v"
     | 12 => "\\f"
     | 13 => "\\r"
     | c =>
         if c < 32 then "\\^" ^ chr (c + 64)
         else if c < 127 then s
         else "\\" ^ string_of_int c)
   else error ("Bad character: " ^ quote s);
 
 fun print_symbol s =
   if Symbol.is_char s then print_symbol_char s
   else if Symbol.is_utf8 s then translate_string print_symbol_char s
   else s;
 
 val print_string = quote o implode o map print_symbol o Symbol.explode;
 val print_strings = print_list print_string;
 
 fun print_path path =
   "Path.explode " ^ print_string (Path.implode path);
 
+val print_platform_path = print_string o File.platform_path;
+
 val print_properties = print_list (print_pair print_string print_string);
 
 fun print_position pos =
   "Position.of_properties " ^ print_properties (Position.properties_of pos);
 
 fun print_range range =
   "Position.range_of_properties " ^ print_properties (Position.properties_of_range range);
 
 fun print_path_binding binding =
   "Path.binding " ^ print_pair print_path print_position (Path.dest_binding binding);
 
 fun make_binding (name, pos) =
   "Binding.make " ^ print_pair print_string print_position (name, pos);
 
 val print_indexname = print_pair print_string print_int;
 
 val print_class = print_string;
 val print_sort = print_list print_class;
 
 fun print_typ (Type arg) = "Term.Type " ^ print_pair print_string (print_list print_typ) arg
   | print_typ (TFree arg) = "Term.TFree " ^ print_pair print_string print_sort arg
   | print_typ (TVar arg) = "Term.TVar " ^ print_pair print_indexname print_sort arg;
 
 fun print_term (Const arg) = "Term.Const " ^ print_pair print_string print_typ arg
   | print_term (Free arg) = "Term.Free " ^ print_pair print_string print_typ arg
   | print_term (Var arg) = "Term.Var " ^ print_pair print_indexname print_typ arg
   | print_term (Bound i) = "Term.Bound " ^ print_int i
   | print_term (Abs (s, T, t)) =
       "Term.Abs (" ^ print_string s ^ ", " ^ print_typ T ^ ", " ^ print_term t ^ ")"
   | print_term (t1 $ t2) = "Term.$ " ^ print_pair print_term print_term (t1, t2);
 
 
 (* toplevel pretty printing *)
 
 fun pretty_string max_len str =
   let
     val body =
       if YXML.is_wellformed str then
         maps (fn XML.Elem _ => ["<markup>"] | XML.Text s => Symbol.explode s) (YXML.parse_body str)
       else Symbol.explode str;
     val body' =
       if length body <= max_len then body
       else take (Int.max (max_len, 0)) body @ ["..."];
   in Pretty.str (quote (implode (map print_symbol body'))) end;
 
 val _ =
   ML_system_pp (fn depth => fn _ => fn str =>
     Pretty.to_polyml (pretty_string (FixedInt.toInt (depth * 100)) str));
 
 end;