clarified file names;
authorwenzelm
Wed Feb 17 23:15:47 2016 +0100 (2016-02-17)
changeset 6235500f7618a9f2b
parent 62354 fdd6989cc8a0
child 62356 e307a410f46c
clarified file names;
src/Pure/ML/exn_output.ML
src/Pure/ML/exn_output_polyml.ML
src/Pure/ML/exn_properties.ML
src/Pure/ML/exn_properties_polyml.ML
src/Pure/ML/ml_compiler.ML
src/Pure/ML/ml_compiler_polyml.ML
src/Pure/ROOT
src/Pure/ROOT.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/ML/exn_output.ML	Wed Feb 17 23:15:47 2016 +0100
     1.3 @@ -0,0 +1,24 @@
     1.4 +(*  Title:      Pure/ML/exn_output.ML
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +Auxiliary operations for exception output.
     1.8 +*)
     1.9 +
    1.10 +signature EXN_OUTPUT =
    1.11 +sig
    1.12 +  val position: exn -> Position.T
    1.13 +  val pretty: exn -> Pretty.T
    1.14 +end;
    1.15 +
    1.16 +structure Exn_Output: EXN_OUTPUT =
    1.17 +struct
    1.18 +
    1.19 +fun position exn =
    1.20 +  (case PolyML.exceptionLocation exn of
    1.21 +    NONE => Position.none
    1.22 +  | SOME loc => Exn_Properties.position_of loc);
    1.23 +
    1.24 +fun pretty (exn: exn) =
    1.25 +  Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (exn, ML_Options.get_print_depth ())));
    1.26 +
    1.27 +end;
     2.1 --- a/src/Pure/ML/exn_output_polyml.ML	Wed Feb 17 23:06:24 2016 +0100
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,24 +0,0 @@
     2.4 -(*  Title:      Pure/ML/exn_output_polyml.ML
     2.5 -    Author:     Makarius
     2.6 -
     2.7 -Auxiliary operations for exception output -- Poly/ML version.
     2.8 -*)
     2.9 -
    2.10 -signature EXN_OUTPUT =
    2.11 -sig
    2.12 -  val position: exn -> Position.T
    2.13 -  val pretty: exn -> Pretty.T
    2.14 -end;
    2.15 -
    2.16 -structure Exn_Output: EXN_OUTPUT =
    2.17 -struct
    2.18 -
    2.19 -fun position exn =
    2.20 -  (case PolyML.exceptionLocation exn of
    2.21 -    NONE => Position.none
    2.22 -  | SOME loc => Exn_Properties.position_of loc);
    2.23 -
    2.24 -fun pretty (exn: exn) =
    2.25 -  Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (exn, ML_Options.get_print_depth ())));
    2.26 -
    2.27 -end;
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Pure/ML/exn_properties.ML	Wed Feb 17 23:15:47 2016 +0100
     3.3 @@ -0,0 +1,63 @@
     3.4 +(*  Title:      Pure/ML/exn_properties.ML
     3.5 +    Author:     Makarius
     3.6 +
     3.7 +Exception properties.
     3.8 +*)
     3.9 +
    3.10 +signature EXN_PROPERTIES =
    3.11 +sig
    3.12 +  val position_of: PolyML.location -> Position.T
    3.13 +  val get: exn -> Properties.T
    3.14 +  val update: Properties.entry list -> exn -> exn
    3.15 +end;
    3.16 +
    3.17 +structure Exn_Properties: EXN_PROPERTIES =
    3.18 +struct
    3.19 +
    3.20 +(* source locations *)
    3.21 +
    3.22 +fun props_of (loc: PolyML.location) =
    3.23 +  (case YXML.parse_body (#file loc) of
    3.24 +    [] => []
    3.25 +  | [XML.Text file] =>
    3.26 +      if file = "Standard Basis" then []
    3.27 +      else [(Markup.fileN, ml_standard_path file)]
    3.28 +  | body => XML.Decode.properties body);
    3.29 +
    3.30 +fun position_of loc =
    3.31 +  Position.make
    3.32 +   {line = #startLine loc,
    3.33 +    offset = #startPosition loc,
    3.34 +    end_offset = #endPosition loc,
    3.35 +    props = props_of loc};
    3.36 +
    3.37 +
    3.38 +(* exception properties *)
    3.39 +
    3.40 +fun get exn =
    3.41 +  (case PolyML.exceptionLocation exn of
    3.42 +    NONE => []
    3.43 +  | SOME loc => props_of loc);
    3.44 +
    3.45 +fun update entries exn =
    3.46 +  let
    3.47 +    val loc =
    3.48 +      the_default {file = "", startLine = 0, endLine = 0, startPosition = 0, endPosition = 0}
    3.49 +        (PolyML.exceptionLocation exn);
    3.50 +    val props = props_of loc;
    3.51 +    val props' = fold Properties.put entries props;
    3.52 +  in
    3.53 +    if props = props' then exn
    3.54 +    else
    3.55 +      let
    3.56 +        val loc' =
    3.57 +          {file = YXML.string_of_body (XML.Encode.properties props'),
    3.58 +            startLine = #startLine loc, endLine = #endLine loc,
    3.59 +            startPosition = #startPosition loc, endPosition = #endPosition loc};
    3.60 +      in
    3.61 +        uninterruptible (fn _ => fn () => PolyML.raiseWithLocation (exn, loc')) ()
    3.62 +          handle exn' => exn'
    3.63 +      end
    3.64 +  end;
    3.65 +
    3.66 +end;
     4.1 --- a/src/Pure/ML/exn_properties_polyml.ML	Wed Feb 17 23:06:24 2016 +0100
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,64 +0,0 @@
     4.4 -(*  Title:      Pure/ML/exn_properties_polyml.ML
     4.5 -    Author:     Makarius
     4.6 -
     4.7 -Exception properties for Poly/ML.
     4.8 -*)
     4.9 -
    4.10 -signature EXN_PROPERTIES =
    4.11 -sig
    4.12 -  val position_of: PolyML.location -> Position.T
    4.13 -  val get: exn -> Properties.T
    4.14 -  val update: Properties.entry list -> exn -> exn
    4.15 -end;
    4.16 -
    4.17 -structure Exn_Properties: EXN_PROPERTIES =
    4.18 -struct
    4.19 -
    4.20 -(* source locations *)
    4.21 -
    4.22 -fun props_of (loc: PolyML.location) =
    4.23 -  (case YXML.parse_body (#file loc) of
    4.24 -    [] => []
    4.25 -  | [XML.Text file] =>
    4.26 -      if file = "Standard Basis" then []
    4.27 -      else [(Markup.fileN, ml_standard_path file)]
    4.28 -  | body => XML.Decode.properties body);
    4.29 -
    4.30 -fun position_of loc =
    4.31 -  Position.make
    4.32 -   {line = #startLine loc,
    4.33 -    offset = #startPosition loc,
    4.34 -    end_offset = #endPosition loc,
    4.35 -    props = props_of loc};
    4.36 -
    4.37 -
    4.38 -(* exception properties *)
    4.39 -
    4.40 -fun get exn =
    4.41 -  (case PolyML.exceptionLocation exn of
    4.42 -    NONE => []
    4.43 -  | SOME loc => props_of loc);
    4.44 -
    4.45 -fun update entries exn =
    4.46 -  let
    4.47 -    val loc =
    4.48 -      the_default {file = "", startLine = 0, endLine = 0, startPosition = 0, endPosition = 0}
    4.49 -        (PolyML.exceptionLocation exn);
    4.50 -    val props = props_of loc;
    4.51 -    val props' = fold Properties.put entries props;
    4.52 -  in
    4.53 -    if props = props' then exn
    4.54 -    else
    4.55 -      let
    4.56 -        val loc' =
    4.57 -          {file = YXML.string_of_body (XML.Encode.properties props'),
    4.58 -            startLine = #startLine loc, endLine = #endLine loc,
    4.59 -            startPosition = #startPosition loc, endPosition = #endPosition loc};
    4.60 -      in
    4.61 -        uninterruptible (fn _ => fn () => PolyML.raiseWithLocation (exn, loc')) ()
    4.62 -          handle exn' => exn'
    4.63 -      end
    4.64 -  end;
    4.65 -
    4.66 -end;
    4.67 -
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/Pure/ML/ml_compiler.ML	Wed Feb 17 23:15:47 2016 +0100
     5.3 @@ -0,0 +1,288 @@
     5.4 +(*  Title:      Pure/ML/ml_compiler.ML
     5.5 +    Author:     Makarius
     5.6 +
     5.7 +Runtime compilation and evaluation.
     5.8 +*)
     5.9 +
    5.10 +signature ML_COMPILER =
    5.11 +sig
    5.12 +  type flags =
    5.13 +    {SML: bool, exchange: bool, redirect: bool, verbose: bool,
    5.14 +      debug: bool option, writeln: string -> unit, warning: string -> unit}
    5.15 +  val flags: flags
    5.16 +  val verbose: bool -> flags -> flags
    5.17 +  val eval: flags -> Position.T -> ML_Lex.token list -> unit
    5.18 +end
    5.19 +
    5.20 +
    5.21 +structure ML_Compiler: ML_COMPILER =
    5.22 +struct
    5.23 +
    5.24 +(* flags *)
    5.25 +
    5.26 +type flags =
    5.27 +  {SML: bool, exchange: bool, redirect: bool, verbose: bool,
    5.28 +    debug: bool option, writeln: string -> unit, warning: string -> unit};
    5.29 +
    5.30 +val flags: flags =
    5.31 +  {SML = false, exchange = false, redirect = false, verbose = false,
    5.32 +    debug = NONE, writeln = writeln, warning = warning};
    5.33 +
    5.34 +fun verbose b (flags: flags) =
    5.35 +  {SML = #SML flags, exchange = #exchange flags, redirect = #redirect flags,
    5.36 +    verbose = b, debug = #debug flags, writeln = #writeln flags, warning = #warning flags};
    5.37 +
    5.38 +
    5.39 +(* parse trees *)
    5.40 +
    5.41 +fun breakpoint_position loc =
    5.42 +  let val pos = Position.reset_range (Exn_Properties.position_of loc) in
    5.43 +    (case Position.offset_of pos of
    5.44 +      NONE => pos
    5.45 +    | SOME 1 => pos
    5.46 +    | SOME j =>
    5.47 +        Position.properties_of pos
    5.48 +        |> Properties.put (Markup.offsetN, Markup.print_int (j - 1))
    5.49 +        |> Position.of_properties)
    5.50 +  end;
    5.51 +
    5.52 +fun report_parse_tree redirect depth space parse_tree =
    5.53 +  let
    5.54 +    val is_visible =
    5.55 +      (case Context.thread_data () of
    5.56 +        SOME context => Context_Position.is_visible_generic context
    5.57 +      | NONE => true);
    5.58 +    fun is_reported pos = is_visible andalso Position.is_reported pos;
    5.59 +
    5.60 +
    5.61 +    (* syntax reports *)
    5.62 +
    5.63 +    fun reported_types loc types =
    5.64 +      let val pos = Exn_Properties.position_of loc in
    5.65 +        is_reported pos ?
    5.66 +          let
    5.67 +            val xml =
    5.68 +              ML_Name_Space.displayTypeExpression (types, depth, space)
    5.69 +              |> pretty_ml |> Pretty.from_ML |> Pretty.string_of
    5.70 +              |> Output.output |> YXML.parse_body;
    5.71 +          in cons (pos, fn () => Markup.ML_typing, fn () => YXML.string_of_body xml) end
    5.72 +      end;
    5.73 +
    5.74 +    fun reported_entity kind loc decl =
    5.75 +      let
    5.76 +        val pos = Exn_Properties.position_of loc;
    5.77 +        val def_pos = Exn_Properties.position_of decl;
    5.78 +      in
    5.79 +        (is_reported pos andalso pos <> def_pos) ?
    5.80 +          let
    5.81 +            fun markup () =
    5.82 +              (Markup.entityN, (Markup.kindN, kind) :: Position.def_properties_of def_pos);
    5.83 +          in cons (pos, markup, fn () => "") end
    5.84 +      end;
    5.85 +
    5.86 +    fun reported_completions loc names =
    5.87 +      let val pos = Exn_Properties.position_of loc in
    5.88 +        if is_reported pos andalso not (null names) then
    5.89 +          let
    5.90 +            val completion = Completion.names pos (map (fn a => (a, ("ML", a))) names);
    5.91 +            val xml = Completion.encode completion;
    5.92 +          in cons (pos, fn () => Markup.completion, fn () => YXML.string_of_body xml) end
    5.93 +        else I
    5.94 +      end;
    5.95 +
    5.96 +    fun reported _ (PolyML.PTnextSibling tree) = reported_tree (tree ())
    5.97 +      | reported _ (PolyML.PTfirstChild tree) = reported_tree (tree ())
    5.98 +      | reported loc (PolyML.PTtype types) = reported_types loc types
    5.99 +      | reported loc (PolyML.PTdeclaredAt decl) = reported_entity Markup.ML_defN loc decl
   5.100 +      | reported loc (PolyML.PTopenedAt decl) = reported_entity Markup.ML_openN loc decl
   5.101 +      | reported loc (PolyML.PTstructureAt decl) = reported_entity Markup.ML_structureN loc decl
   5.102 +      | reported loc pt =
   5.103 +          (case ML_Parse_Tree.completions pt of
   5.104 +            SOME names => reported_completions loc names
   5.105 +          | NONE => I)
   5.106 +    and reported_tree (loc, props) = fold (reported loc) props;
   5.107 +
   5.108 +    val persistent_reports = reported_tree parse_tree [];
   5.109 +
   5.110 +    fun output () =
   5.111 +      persistent_reports
   5.112 +      |> map (fn (pos, markup, text) => Position.reported_text pos (markup ()) (text ()))
   5.113 +      |> Output.report;
   5.114 +    val _ =
   5.115 +      if not (null persistent_reports) andalso redirect andalso Multithreading.enabled ()
   5.116 +      then
   5.117 +        Execution.print
   5.118 +          {name = "ML_Compiler.report", pos = Position.thread_data (), pri = Task_Queue.urgent_pri}
   5.119 +          output
   5.120 +      else output ();
   5.121 +
   5.122 +
   5.123 +    (* breakpoints *)
   5.124 +
   5.125 +    fun breakpoints _ (PolyML.PTnextSibling tree) = breakpoints_tree (tree ())
   5.126 +      | breakpoints _ (PolyML.PTfirstChild tree) = breakpoints_tree (tree ())
   5.127 +      | breakpoints loc pt =
   5.128 +          (case ML_Parse_Tree.breakpoint pt of
   5.129 +            SOME b =>
   5.130 +              let val pos = breakpoint_position loc in
   5.131 +                if is_reported pos then
   5.132 +                  let val id = serial ();
   5.133 +                  in cons ((pos, Markup.ML_breakpoint id), (id, (b, pos))) end
   5.134 +                else I
   5.135 +              end
   5.136 +          | NONE => I)
   5.137 +    and breakpoints_tree (loc, props) = fold (breakpoints loc) props;
   5.138 +
   5.139 +    val all_breakpoints = rev (breakpoints_tree parse_tree []);
   5.140 +    val _ = Position.reports (map #1 all_breakpoints);
   5.141 +    val _ =
   5.142 +      if is_some (Context.thread_data ()) then
   5.143 +        Context.>> (fold (ML_Env.add_breakpoint o #2) all_breakpoints)
   5.144 +      else ();
   5.145 +  in () end;
   5.146 +
   5.147 +
   5.148 +(* eval ML source tokens *)
   5.149 +
   5.150 +fun eval (flags: flags) pos toks =
   5.151 +  let
   5.152 +    val _ = Secure.secure_mltext ();
   5.153 +    val space = ML_Env.name_space {SML = #SML flags, exchange = #exchange flags};
   5.154 +    val opt_context = Context.thread_data ();
   5.155 +
   5.156 +
   5.157 +    (* input *)
   5.158 +
   5.159 +    val location_props = op ^ (YXML.output_markup (":", #props (Position.dest pos)));
   5.160 +
   5.161 +    val input_explode =
   5.162 +      if #SML flags then String.explode
   5.163 +      else maps (String.explode o Symbol.esc) o Symbol.explode;
   5.164 +
   5.165 +    val input_buffer =
   5.166 +      Unsynchronized.ref (toks |> map (`(input_explode o ML_Lex.check_content_of)));
   5.167 +
   5.168 +    fun get () =
   5.169 +      (case ! input_buffer of
   5.170 +        (c :: cs, tok) :: rest => (input_buffer := (cs, tok) :: rest; SOME c)
   5.171 +      | ([], _) :: rest => (input_buffer := rest; SOME #" ")
   5.172 +      | [] => NONE);
   5.173 +
   5.174 +    fun get_pos () =
   5.175 +      (case ! input_buffer of
   5.176 +        (_ :: _, tok) :: _ => ML_Lex.pos_of tok
   5.177 +      | ([], tok) :: _ => ML_Lex.end_pos_of tok
   5.178 +      | [] => Position.none);
   5.179 +
   5.180 +
   5.181 +    (* output *)
   5.182 +
   5.183 +    val writeln_buffer = Unsynchronized.ref Buffer.empty;
   5.184 +    fun write s = Unsynchronized.change writeln_buffer (Buffer.add s);
   5.185 +    fun output_writeln () = #writeln flags (trim_line (Buffer.content (! writeln_buffer)));
   5.186 +
   5.187 +    val warnings = Unsynchronized.ref ([]: string list);
   5.188 +    fun warn msg = Unsynchronized.change warnings (cons msg);
   5.189 +    fun output_warnings () = List.app (#warning flags) (rev (! warnings));
   5.190 +
   5.191 +    val error_buffer = Unsynchronized.ref Buffer.empty;
   5.192 +    fun err msg = Unsynchronized.change error_buffer (Buffer.add msg #> Buffer.add "\n");
   5.193 +    fun flush_error () = #writeln flags (trim_line (Buffer.content (! error_buffer)));
   5.194 +    fun raise_error msg = error (trim_line (Buffer.content (Buffer.add msg (! error_buffer))));
   5.195 +
   5.196 +    fun message {message = msg, hard, location = loc, context = _} =
   5.197 +      let
   5.198 +        val pos = Exn_Properties.position_of loc;
   5.199 +        val txt =
   5.200 +          (if hard then "ML error" else "ML warning") ^ Position.here pos ^ ":\n" ^
   5.201 +          Pretty.string_of (Pretty.from_ML (pretty_ml msg));
   5.202 +      in if hard then err txt else warn txt end;
   5.203 +
   5.204 +
   5.205 +    (* results *)
   5.206 +
   5.207 +    val depth = ML_Options.get_print_depth ();
   5.208 +
   5.209 +    fun apply_result {fixes, types, signatures, structures, functors, values} =
   5.210 +      let
   5.211 +        fun display disp x =
   5.212 +          if depth > 0 then
   5.213 +            (disp x |> pretty_ml |> Pretty.from_ML |> Pretty.string_of |> write; write "\n")
   5.214 +          else ();
   5.215 +
   5.216 +        fun apply_fix (a, b) =
   5.217 +          (#enterFix space (a, b); display ML_Name_Space.displayFix (a, b));
   5.218 +        fun apply_type (a, b) =
   5.219 +          (#enterType space (a, b); display ML_Name_Space.displayType (b, depth, space));
   5.220 +        fun apply_sig (a, b) =
   5.221 +          (#enterSig space (a, b); display ML_Name_Space.displaySig (b, depth, space));
   5.222 +        fun apply_struct (a, b) =
   5.223 +          (#enterStruct space (a, b); display ML_Name_Space.displayStruct (b, depth, space));
   5.224 +        fun apply_funct (a, b) =
   5.225 +          (#enterFunct space (a, b); display ML_Name_Space.displayFunct (b, depth, space));
   5.226 +        fun apply_val (a, b) =
   5.227 +          (#enterVal space (a, b); display ML_Name_Space.displayVal (b, depth, space));
   5.228 +      in
   5.229 +        List.app apply_fix fixes;
   5.230 +        List.app apply_type types;
   5.231 +        List.app apply_sig signatures;
   5.232 +        List.app apply_struct structures;
   5.233 +        List.app apply_funct functors;
   5.234 +        List.app apply_val values
   5.235 +      end;
   5.236 +
   5.237 +    exception STATIC_ERRORS of unit;
   5.238 +
   5.239 +    fun result_fun (phase1, phase2) () =
   5.240 +     ((case phase1 of
   5.241 +        NONE => ()
   5.242 +      | SOME parse_tree => report_parse_tree (#redirect flags) depth space parse_tree);
   5.243 +      (case phase2 of
   5.244 +        NONE => raise STATIC_ERRORS ()
   5.245 +      | SOME code =>
   5.246 +          apply_result
   5.247 +            ((code
   5.248 +              |> Runtime.debugging opt_context
   5.249 +              |> Runtime.toplevel_error (err o Runtime.exn_message)) ())));
   5.250 +
   5.251 +
   5.252 +    (* compiler invocation *)
   5.253 +
   5.254 +    val debug =
   5.255 +      (case #debug flags of
   5.256 +        SOME debug => debug
   5.257 +      | NONE => ML_Options.debugger_enabled opt_context);
   5.258 +
   5.259 +    val parameters =
   5.260 +     [PolyML.Compiler.CPOutStream write,
   5.261 +      PolyML.Compiler.CPNameSpace space,
   5.262 +      PolyML.Compiler.CPErrorMessageProc message,
   5.263 +      PolyML.Compiler.CPLineNo (the_default 0 o Position.line_of o get_pos),
   5.264 +      PolyML.Compiler.CPLineOffset (the_default 0 o Position.offset_of o get_pos),
   5.265 +      PolyML.Compiler.CPFileName location_props,
   5.266 +      PolyML.Compiler.CPPrintDepth ML_Options.get_print_depth,
   5.267 +      PolyML.Compiler.CPCompilerResultFun result_fun,
   5.268 +      PolyML.Compiler.CPPrintInAlphabeticalOrder false] @
   5.269 +     ML_Compiler_Parameters.debug debug;
   5.270 +
   5.271 +    val _ =
   5.272 +      (while not (List.null (! input_buffer)) do
   5.273 +        PolyML.compiler (get, parameters) ())
   5.274 +      handle exn =>
   5.275 +        if Exn.is_interrupt exn then reraise exn
   5.276 +        else
   5.277 +          let
   5.278 +            val exn_msg =
   5.279 +              (case exn of
   5.280 +                STATIC_ERRORS () => ""
   5.281 +              | Runtime.TOPLEVEL_ERROR => ""
   5.282 +              | _ => "Exception- " ^ Pretty.string_of (Exn_Output.pretty exn) ^ " raised");
   5.283 +            val _ = output_warnings ();
   5.284 +            val _ = output_writeln ();
   5.285 +          in raise_error exn_msg end;
   5.286 +  in
   5.287 +    if #verbose flags then (output_warnings (); flush_error (); output_writeln ())
   5.288 +    else ()
   5.289 +  end;
   5.290 +
   5.291 +end;
     6.1 --- a/src/Pure/ML/ml_compiler_polyml.ML	Wed Feb 17 23:06:24 2016 +0100
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,288 +0,0 @@
     6.4 -(*  Title:      Pure/ML/ml_compiler_polyml.ML
     6.5 -    Author:     Makarius
     6.6 -
     6.7 -Runtime compilation and evaluation -- Poly/ML version.
     6.8 -*)
     6.9 -
    6.10 -signature ML_COMPILER =
    6.11 -sig
    6.12 -  type flags =
    6.13 -    {SML: bool, exchange: bool, redirect: bool, verbose: bool,
    6.14 -      debug: bool option, writeln: string -> unit, warning: string -> unit}
    6.15 -  val flags: flags
    6.16 -  val verbose: bool -> flags -> flags
    6.17 -  val eval: flags -> Position.T -> ML_Lex.token list -> unit
    6.18 -end
    6.19 -
    6.20 -
    6.21 -structure ML_Compiler: ML_COMPILER =
    6.22 -struct
    6.23 -
    6.24 -(* flags *)
    6.25 -
    6.26 -type flags =
    6.27 -  {SML: bool, exchange: bool, redirect: bool, verbose: bool,
    6.28 -    debug: bool option, writeln: string -> unit, warning: string -> unit};
    6.29 -
    6.30 -val flags: flags =
    6.31 -  {SML = false, exchange = false, redirect = false, verbose = false,
    6.32 -    debug = NONE, writeln = writeln, warning = warning};
    6.33 -
    6.34 -fun verbose b (flags: flags) =
    6.35 -  {SML = #SML flags, exchange = #exchange flags, redirect = #redirect flags,
    6.36 -    verbose = b, debug = #debug flags, writeln = #writeln flags, warning = #warning flags};
    6.37 -
    6.38 -
    6.39 -(* parse trees *)
    6.40 -
    6.41 -fun breakpoint_position loc =
    6.42 -  let val pos = Position.reset_range (Exn_Properties.position_of loc) in
    6.43 -    (case Position.offset_of pos of
    6.44 -      NONE => pos
    6.45 -    | SOME 1 => pos
    6.46 -    | SOME j =>
    6.47 -        Position.properties_of pos
    6.48 -        |> Properties.put (Markup.offsetN, Markup.print_int (j - 1))
    6.49 -        |> Position.of_properties)
    6.50 -  end;
    6.51 -
    6.52 -fun report_parse_tree redirect depth space parse_tree =
    6.53 -  let
    6.54 -    val is_visible =
    6.55 -      (case Context.thread_data () of
    6.56 -        SOME context => Context_Position.is_visible_generic context
    6.57 -      | NONE => true);
    6.58 -    fun is_reported pos = is_visible andalso Position.is_reported pos;
    6.59 -
    6.60 -
    6.61 -    (* syntax reports *)
    6.62 -
    6.63 -    fun reported_types loc types =
    6.64 -      let val pos = Exn_Properties.position_of loc in
    6.65 -        is_reported pos ?
    6.66 -          let
    6.67 -            val xml =
    6.68 -              ML_Name_Space.displayTypeExpression (types, depth, space)
    6.69 -              |> pretty_ml |> Pretty.from_ML |> Pretty.string_of
    6.70 -              |> Output.output |> YXML.parse_body;
    6.71 -          in cons (pos, fn () => Markup.ML_typing, fn () => YXML.string_of_body xml) end
    6.72 -      end;
    6.73 -
    6.74 -    fun reported_entity kind loc decl =
    6.75 -      let
    6.76 -        val pos = Exn_Properties.position_of loc;
    6.77 -        val def_pos = Exn_Properties.position_of decl;
    6.78 -      in
    6.79 -        (is_reported pos andalso pos <> def_pos) ?
    6.80 -          let
    6.81 -            fun markup () =
    6.82 -              (Markup.entityN, (Markup.kindN, kind) :: Position.def_properties_of def_pos);
    6.83 -          in cons (pos, markup, fn () => "") end
    6.84 -      end;
    6.85 -
    6.86 -    fun reported_completions loc names =
    6.87 -      let val pos = Exn_Properties.position_of loc in
    6.88 -        if is_reported pos andalso not (null names) then
    6.89 -          let
    6.90 -            val completion = Completion.names pos (map (fn a => (a, ("ML", a))) names);
    6.91 -            val xml = Completion.encode completion;
    6.92 -          in cons (pos, fn () => Markup.completion, fn () => YXML.string_of_body xml) end
    6.93 -        else I
    6.94 -      end;
    6.95 -
    6.96 -    fun reported _ (PolyML.PTnextSibling tree) = reported_tree (tree ())
    6.97 -      | reported _ (PolyML.PTfirstChild tree) = reported_tree (tree ())
    6.98 -      | reported loc (PolyML.PTtype types) = reported_types loc types
    6.99 -      | reported loc (PolyML.PTdeclaredAt decl) = reported_entity Markup.ML_defN loc decl
   6.100 -      | reported loc (PolyML.PTopenedAt decl) = reported_entity Markup.ML_openN loc decl
   6.101 -      | reported loc (PolyML.PTstructureAt decl) = reported_entity Markup.ML_structureN loc decl
   6.102 -      | reported loc pt =
   6.103 -          (case ML_Parse_Tree.completions pt of
   6.104 -            SOME names => reported_completions loc names
   6.105 -          | NONE => I)
   6.106 -    and reported_tree (loc, props) = fold (reported loc) props;
   6.107 -
   6.108 -    val persistent_reports = reported_tree parse_tree [];
   6.109 -
   6.110 -    fun output () =
   6.111 -      persistent_reports
   6.112 -      |> map (fn (pos, markup, text) => Position.reported_text pos (markup ()) (text ()))
   6.113 -      |> Output.report;
   6.114 -    val _ =
   6.115 -      if not (null persistent_reports) andalso redirect andalso Multithreading.enabled ()
   6.116 -      then
   6.117 -        Execution.print
   6.118 -          {name = "ML_Compiler.report", pos = Position.thread_data (), pri = Task_Queue.urgent_pri}
   6.119 -          output
   6.120 -      else output ();
   6.121 -
   6.122 -
   6.123 -    (* breakpoints *)
   6.124 -
   6.125 -    fun breakpoints _ (PolyML.PTnextSibling tree) = breakpoints_tree (tree ())
   6.126 -      | breakpoints _ (PolyML.PTfirstChild tree) = breakpoints_tree (tree ())
   6.127 -      | breakpoints loc pt =
   6.128 -          (case ML_Parse_Tree.breakpoint pt of
   6.129 -            SOME b =>
   6.130 -              let val pos = breakpoint_position loc in
   6.131 -                if is_reported pos then
   6.132 -                  let val id = serial ();
   6.133 -                  in cons ((pos, Markup.ML_breakpoint id), (id, (b, pos))) end
   6.134 -                else I
   6.135 -              end
   6.136 -          | NONE => I)
   6.137 -    and breakpoints_tree (loc, props) = fold (breakpoints loc) props;
   6.138 -
   6.139 -    val all_breakpoints = rev (breakpoints_tree parse_tree []);
   6.140 -    val _ = Position.reports (map #1 all_breakpoints);
   6.141 -    val _ =
   6.142 -      if is_some (Context.thread_data ()) then
   6.143 -        Context.>> (fold (ML_Env.add_breakpoint o #2) all_breakpoints)
   6.144 -      else ();
   6.145 -  in () end;
   6.146 -
   6.147 -
   6.148 -(* eval ML source tokens *)
   6.149 -
   6.150 -fun eval (flags: flags) pos toks =
   6.151 -  let
   6.152 -    val _ = Secure.secure_mltext ();
   6.153 -    val space = ML_Env.name_space {SML = #SML flags, exchange = #exchange flags};
   6.154 -    val opt_context = Context.thread_data ();
   6.155 -
   6.156 -
   6.157 -    (* input *)
   6.158 -
   6.159 -    val location_props = op ^ (YXML.output_markup (":", #props (Position.dest pos)));
   6.160 -
   6.161 -    val input_explode =
   6.162 -      if #SML flags then String.explode
   6.163 -      else maps (String.explode o Symbol.esc) o Symbol.explode;
   6.164 -
   6.165 -    val input_buffer =
   6.166 -      Unsynchronized.ref (toks |> map (`(input_explode o ML_Lex.check_content_of)));
   6.167 -
   6.168 -    fun get () =
   6.169 -      (case ! input_buffer of
   6.170 -        (c :: cs, tok) :: rest => (input_buffer := (cs, tok) :: rest; SOME c)
   6.171 -      | ([], _) :: rest => (input_buffer := rest; SOME #" ")
   6.172 -      | [] => NONE);
   6.173 -
   6.174 -    fun get_pos () =
   6.175 -      (case ! input_buffer of
   6.176 -        (_ :: _, tok) :: _ => ML_Lex.pos_of tok
   6.177 -      | ([], tok) :: _ => ML_Lex.end_pos_of tok
   6.178 -      | [] => Position.none);
   6.179 -
   6.180 -
   6.181 -    (* output *)
   6.182 -
   6.183 -    val writeln_buffer = Unsynchronized.ref Buffer.empty;
   6.184 -    fun write s = Unsynchronized.change writeln_buffer (Buffer.add s);
   6.185 -    fun output_writeln () = #writeln flags (trim_line (Buffer.content (! writeln_buffer)));
   6.186 -
   6.187 -    val warnings = Unsynchronized.ref ([]: string list);
   6.188 -    fun warn msg = Unsynchronized.change warnings (cons msg);
   6.189 -    fun output_warnings () = List.app (#warning flags) (rev (! warnings));
   6.190 -
   6.191 -    val error_buffer = Unsynchronized.ref Buffer.empty;
   6.192 -    fun err msg = Unsynchronized.change error_buffer (Buffer.add msg #> Buffer.add "\n");
   6.193 -    fun flush_error () = #writeln flags (trim_line (Buffer.content (! error_buffer)));
   6.194 -    fun raise_error msg = error (trim_line (Buffer.content (Buffer.add msg (! error_buffer))));
   6.195 -
   6.196 -    fun message {message = msg, hard, location = loc, context = _} =
   6.197 -      let
   6.198 -        val pos = Exn_Properties.position_of loc;
   6.199 -        val txt =
   6.200 -          (if hard then "ML error" else "ML warning") ^ Position.here pos ^ ":\n" ^
   6.201 -          Pretty.string_of (Pretty.from_ML (pretty_ml msg));
   6.202 -      in if hard then err txt else warn txt end;
   6.203 -
   6.204 -
   6.205 -    (* results *)
   6.206 -
   6.207 -    val depth = ML_Options.get_print_depth ();
   6.208 -
   6.209 -    fun apply_result {fixes, types, signatures, structures, functors, values} =
   6.210 -      let
   6.211 -        fun display disp x =
   6.212 -          if depth > 0 then
   6.213 -            (disp x |> pretty_ml |> Pretty.from_ML |> Pretty.string_of |> write; write "\n")
   6.214 -          else ();
   6.215 -
   6.216 -        fun apply_fix (a, b) =
   6.217 -          (#enterFix space (a, b); display ML_Name_Space.displayFix (a, b));
   6.218 -        fun apply_type (a, b) =
   6.219 -          (#enterType space (a, b); display ML_Name_Space.displayType (b, depth, space));
   6.220 -        fun apply_sig (a, b) =
   6.221 -          (#enterSig space (a, b); display ML_Name_Space.displaySig (b, depth, space));
   6.222 -        fun apply_struct (a, b) =
   6.223 -          (#enterStruct space (a, b); display ML_Name_Space.displayStruct (b, depth, space));
   6.224 -        fun apply_funct (a, b) =
   6.225 -          (#enterFunct space (a, b); display ML_Name_Space.displayFunct (b, depth, space));
   6.226 -        fun apply_val (a, b) =
   6.227 -          (#enterVal space (a, b); display ML_Name_Space.displayVal (b, depth, space));
   6.228 -      in
   6.229 -        List.app apply_fix fixes;
   6.230 -        List.app apply_type types;
   6.231 -        List.app apply_sig signatures;
   6.232 -        List.app apply_struct structures;
   6.233 -        List.app apply_funct functors;
   6.234 -        List.app apply_val values
   6.235 -      end;
   6.236 -
   6.237 -    exception STATIC_ERRORS of unit;
   6.238 -
   6.239 -    fun result_fun (phase1, phase2) () =
   6.240 -     ((case phase1 of
   6.241 -        NONE => ()
   6.242 -      | SOME parse_tree => report_parse_tree (#redirect flags) depth space parse_tree);
   6.243 -      (case phase2 of
   6.244 -        NONE => raise STATIC_ERRORS ()
   6.245 -      | SOME code =>
   6.246 -          apply_result
   6.247 -            ((code
   6.248 -              |> Runtime.debugging opt_context
   6.249 -              |> Runtime.toplevel_error (err o Runtime.exn_message)) ())));
   6.250 -
   6.251 -
   6.252 -    (* compiler invocation *)
   6.253 -
   6.254 -    val debug =
   6.255 -      (case #debug flags of
   6.256 -        SOME debug => debug
   6.257 -      | NONE => ML_Options.debugger_enabled opt_context);
   6.258 -
   6.259 -    val parameters =
   6.260 -     [PolyML.Compiler.CPOutStream write,
   6.261 -      PolyML.Compiler.CPNameSpace space,
   6.262 -      PolyML.Compiler.CPErrorMessageProc message,
   6.263 -      PolyML.Compiler.CPLineNo (the_default 0 o Position.line_of o get_pos),
   6.264 -      PolyML.Compiler.CPLineOffset (the_default 0 o Position.offset_of o get_pos),
   6.265 -      PolyML.Compiler.CPFileName location_props,
   6.266 -      PolyML.Compiler.CPPrintDepth ML_Options.get_print_depth,
   6.267 -      PolyML.Compiler.CPCompilerResultFun result_fun,
   6.268 -      PolyML.Compiler.CPPrintInAlphabeticalOrder false] @
   6.269 -     ML_Compiler_Parameters.debug debug;
   6.270 -
   6.271 -    val _ =
   6.272 -      (while not (List.null (! input_buffer)) do
   6.273 -        PolyML.compiler (get, parameters) ())
   6.274 -      handle exn =>
   6.275 -        if Exn.is_interrupt exn then reraise exn
   6.276 -        else
   6.277 -          let
   6.278 -            val exn_msg =
   6.279 -              (case exn of
   6.280 -                STATIC_ERRORS () => ""
   6.281 -              | Runtime.TOPLEVEL_ERROR => ""
   6.282 -              | _ => "Exception- " ^ Pretty.string_of (Exn_Output.pretty exn) ^ " raised");
   6.283 -            val _ = output_warnings ();
   6.284 -            val _ = output_writeln ();
   6.285 -          in raise_error exn_msg end;
   6.286 -  in
   6.287 -    if #verbose flags then (output_warnings (); flush_error (); output_writeln ())
   6.288 -    else ()
   6.289 -  end;
   6.290 -
   6.291 -end;
     7.1 --- a/src/Pure/ROOT	Wed Feb 17 23:06:24 2016 +0100
     7.2 +++ b/src/Pure/ROOT	Wed Feb 17 23:15:47 2016 +0100
     7.3 @@ -163,11 +163,11 @@
     7.4      "Isar/token.ML"
     7.5      "Isar/toplevel.ML"
     7.6      "Isar/typedecl.ML"
     7.7 -    "ML/exn_output_polyml.ML"
     7.8 -    "ML/exn_properties_polyml.ML"
     7.9 +    "ML/exn_output.ML"
    7.10 +    "ML/exn_properties.ML"
    7.11      "ML/install_pp_polyml.ML"
    7.12      "ML/ml_antiquotation.ML"
    7.13 -    "ML/ml_compiler_polyml.ML"
    7.14 +    "ML/ml_compiler.ML"
    7.15      "ML/ml_context.ML"
    7.16      "ML/ml_env.ML"
    7.17      "ML/ml_file.ML"
     8.1 --- a/src/Pure/ROOT.ML	Wed Feb 17 23:06:24 2016 +0100
     8.2 +++ b/src/Pure/ROOT.ML	Wed Feb 17 23:15:47 2016 +0100
     8.3 @@ -98,7 +98,7 @@
     8.4  
     8.5  (* concurrency within the ML runtime *)
     8.6  
     8.7 -use "ML/exn_properties_polyml.ML";
     8.8 +use "ML/exn_properties.ML";
     8.9  
    8.10  if ML_System.name = "polyml-5.5.0"
    8.11    orelse ML_System.name = "polyml-5.5.1"
    8.12 @@ -200,11 +200,11 @@
    8.13  use "ML/ml_syntax.ML";
    8.14  use "ML/ml_env.ML";
    8.15  use "ML/ml_options.ML";
    8.16 -use "ML/exn_output_polyml.ML";
    8.17 +use "ML/exn_output.ML";
    8.18  use "ML/ml_options.ML";
    8.19  use "Isar/runtime.ML";
    8.20  use "PIDE/execution.ML";
    8.21 -use "ML/ml_compiler_polyml.ML";
    8.22 +use "ML/ml_compiler.ML";
    8.23  
    8.24  use "skip_proof.ML";
    8.25  use "goal.ML";