src/Pure/ML/ml_compiler.ML
author wenzelm
Fri, 18 Mar 2016 16:26:35 +0100
changeset 62663 bea354f6ff21
parent 62516 5732f1c31566
child 62668 360d3464919c
permissions -rw-r--r--
clarified modules; tuned signature;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
62355
00f7618a9f2b clarified file names;
wenzelm
parents: 62354
diff changeset
     1
(*  Title:      Pure/ML/ml_compiler.ML
31333
fcd010617e6c added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
fcd010617e6c added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff changeset
     3
62355
00f7618a9f2b clarified file names;
wenzelm
parents: 62354
diff changeset
     4
Runtime compilation and evaluation.
31333
fcd010617e6c added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff changeset
     5
*)
fcd010617e6c added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff changeset
     6
62354
fdd6989cc8a0 SML/NJ is no longer supported;
wenzelm
parents: 61715
diff changeset
     7
signature ML_COMPILER =
fdd6989cc8a0 SML/NJ is no longer supported;
wenzelm
parents: 61715
diff changeset
     8
sig
fdd6989cc8a0 SML/NJ is no longer supported;
wenzelm
parents: 61715
diff changeset
     9
  type flags =
fdd6989cc8a0 SML/NJ is no longer supported;
wenzelm
parents: 61715
diff changeset
    10
    {SML: bool, exchange: bool, redirect: bool, verbose: bool,
fdd6989cc8a0 SML/NJ is no longer supported;
wenzelm
parents: 61715
diff changeset
    11
      debug: bool option, writeln: string -> unit, warning: string -> unit}
62490
39d01eaf5292 ML debugger support in Pure (again, see 3565c9f407ec);
wenzelm
parents: 62387
diff changeset
    12
  val debug_flags: bool option -> flags
62354
fdd6989cc8a0 SML/NJ is no longer supported;
wenzelm
parents: 61715
diff changeset
    13
  val flags: flags
fdd6989cc8a0 SML/NJ is no longer supported;
wenzelm
parents: 61715
diff changeset
    14
  val verbose: bool -> flags -> flags
fdd6989cc8a0 SML/NJ is no longer supported;
wenzelm
parents: 61715
diff changeset
    15
  val eval: flags -> Position.T -> ML_Lex.token list -> unit
62490
39d01eaf5292 ML debugger support in Pure (again, see 3565c9f407ec);
wenzelm
parents: 62387
diff changeset
    16
end;
62354
fdd6989cc8a0 SML/NJ is no longer supported;
wenzelm
parents: 61715
diff changeset
    17
31333
fcd010617e6c added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff changeset
    18
structure ML_Compiler: ML_COMPILER =
fcd010617e6c added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff changeset
    19
struct
fcd010617e6c added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff changeset
    20
62354
fdd6989cc8a0 SML/NJ is no longer supported;
wenzelm
parents: 61715
diff changeset
    21
(* flags *)
fdd6989cc8a0 SML/NJ is no longer supported;
wenzelm
parents: 61715
diff changeset
    22
fdd6989cc8a0 SML/NJ is no longer supported;
wenzelm
parents: 61715
diff changeset
    23
type flags =
fdd6989cc8a0 SML/NJ is no longer supported;
wenzelm
parents: 61715
diff changeset
    24
  {SML: bool, exchange: bool, redirect: bool, verbose: bool,
fdd6989cc8a0 SML/NJ is no longer supported;
wenzelm
parents: 61715
diff changeset
    25
    debug: bool option, writeln: string -> unit, warning: string -> unit};
fdd6989cc8a0 SML/NJ is no longer supported;
wenzelm
parents: 61715
diff changeset
    26
62490
39d01eaf5292 ML debugger support in Pure (again, see 3565c9f407ec);
wenzelm
parents: 62387
diff changeset
    27
fun debug_flags opt_debug : flags =
62354
fdd6989cc8a0 SML/NJ is no longer supported;
wenzelm
parents: 61715
diff changeset
    28
  {SML = false, exchange = false, redirect = false, verbose = false,
62490
39d01eaf5292 ML debugger support in Pure (again, see 3565c9f407ec);
wenzelm
parents: 62387
diff changeset
    29
    debug = opt_debug, writeln = writeln, warning = warning};
39d01eaf5292 ML debugger support in Pure (again, see 3565c9f407ec);
wenzelm
parents: 62387
diff changeset
    30
39d01eaf5292 ML debugger support in Pure (again, see 3565c9f407ec);
wenzelm
parents: 62387
diff changeset
    31
val flags = debug_flags NONE;
62354
fdd6989cc8a0 SML/NJ is no longer supported;
wenzelm
parents: 61715
diff changeset
    32
fdd6989cc8a0 SML/NJ is no longer supported;
wenzelm
parents: 61715
diff changeset
    33
fun verbose b (flags: flags) =
fdd6989cc8a0 SML/NJ is no longer supported;
wenzelm
parents: 61715
diff changeset
    34
  {SML = #SML flags, exchange = #exchange flags, redirect = #redirect flags,
fdd6989cc8a0 SML/NJ is no longer supported;
wenzelm
parents: 61715
diff changeset
    35
    verbose = b, debug = #debug flags, writeln = #writeln flags, warning = #warning flags};
56281
03c3d1a7c3b8 proper configuration option "ML_print_depth";
wenzelm
parents: 56275
diff changeset
    36
03c3d1a7c3b8 proper configuration option "ML_print_depth";
wenzelm
parents: 56275
diff changeset
    37
31333
fcd010617e6c added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff changeset
    38
(* parse trees *)
fcd010617e6c added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff changeset
    39
60913
7432d6bb4195 clarified breakpoint rendering;
wenzelm
parents: 60894
diff changeset
    40
fun breakpoint_position loc =
62516
5732f1c31566 tuned signature -- clarified modules;
wenzelm
parents: 62505
diff changeset
    41
  let val pos = Position.reset_range (Exn_Properties.position_of_location loc) in
60913
7432d6bb4195 clarified breakpoint rendering;
wenzelm
parents: 60894
diff changeset
    42
    (case Position.offset_of pos of
7432d6bb4195 clarified breakpoint rendering;
wenzelm
parents: 60894
diff changeset
    43
      NONE => pos
7432d6bb4195 clarified breakpoint rendering;
wenzelm
parents: 60894
diff changeset
    44
    | SOME 1 => pos
7432d6bb4195 clarified breakpoint rendering;
wenzelm
parents: 60894
diff changeset
    45
    | SOME j =>
7432d6bb4195 clarified breakpoint rendering;
wenzelm
parents: 60894
diff changeset
    46
        Position.properties_of pos
7432d6bb4195 clarified breakpoint rendering;
wenzelm
parents: 60894
diff changeset
    47
        |> Properties.put (Markup.offsetN, Markup.print_int (j - 1))
7432d6bb4195 clarified breakpoint rendering;
wenzelm
parents: 60894
diff changeset
    48
        |> Position.of_properties)
7432d6bb4195 clarified breakpoint rendering;
wenzelm
parents: 60894
diff changeset
    49
  end;
7432d6bb4195 clarified breakpoint rendering;
wenzelm
parents: 60894
diff changeset
    50
56304
40274e4f5ebf redirect ML_Compiler reports more directly: only the (big) parse tree report is deferred via Execution.print (NB: this does not work for asynchronous "diag" commands);
wenzelm
parents: 56303
diff changeset
    51
fun report_parse_tree redirect depth space parse_tree =
31333
fcd010617e6c added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff changeset
    52
  let
56304
40274e4f5ebf redirect ML_Compiler reports more directly: only the (big) parse tree report is deferred via Execution.print (NB: this does not work for asynchronous "diag" commands);
wenzelm
parents: 56303
diff changeset
    53
    val is_visible =
38720
7f8bc335e203 ML_Context.eval: produce antiquotation environment preferably in invisible context, to avoid displaced report messages from ML_Compiler;
wenzelm
parents: 38228
diff changeset
    54
      (case Context.thread_data () of
56304
40274e4f5ebf redirect ML_Compiler reports more directly: only the (big) parse tree report is deferred via Execution.print (NB: this does not work for asynchronous "diag" commands);
wenzelm
parents: 56303
diff changeset
    55
        SOME context => Context_Position.is_visible_generic context
40274e4f5ebf redirect ML_Compiler reports more directly: only the (big) parse tree report is deferred via Execution.print (NB: this does not work for asynchronous "diag" commands);
wenzelm
parents: 56303
diff changeset
    56
      | NONE => true);
40274e4f5ebf redirect ML_Compiler reports more directly: only the (big) parse tree report is deferred via Execution.print (NB: this does not work for asynchronous "diag" commands);
wenzelm
parents: 56303
diff changeset
    57
    fun is_reported pos = is_visible andalso Position.is_reported pos;
40274e4f5ebf redirect ML_Compiler reports more directly: only the (big) parse tree report is deferred via Execution.print (NB: this does not work for asynchronous "diag" commands);
wenzelm
parents: 56303
diff changeset
    58
60744
4eba53a0ac3d report possible breakpoint positions;
wenzelm
parents: 60732
diff changeset
    59
4eba53a0ac3d report possible breakpoint positions;
wenzelm
parents: 60732
diff changeset
    60
    (* syntax reports *)
4eba53a0ac3d report possible breakpoint positions;
wenzelm
parents: 60732
diff changeset
    61
56304
40274e4f5ebf redirect ML_Compiler reports more directly: only the (big) parse tree report is deferred via Execution.print (NB: this does not work for asynchronous "diag" commands);
wenzelm
parents: 56303
diff changeset
    62
    fun reported_types loc types =
62516
5732f1c31566 tuned signature -- clarified modules;
wenzelm
parents: 62505
diff changeset
    63
      let val pos = Exn_Properties.position_of_location loc in
56304
40274e4f5ebf redirect ML_Compiler reports more directly: only the (big) parse tree report is deferred via Execution.print (NB: this does not work for asynchronous "diag" commands);
wenzelm
parents: 56303
diff changeset
    64
        is_reported pos ?
40274e4f5ebf redirect ML_Compiler reports more directly: only the (big) parse tree report is deferred via Execution.print (NB: this does not work for asynchronous "diag" commands);
wenzelm
parents: 56303
diff changeset
    65
          let
40274e4f5ebf redirect ML_Compiler reports more directly: only the (big) parse tree report is deferred via Execution.print (NB: this does not work for asynchronous "diag" commands);
wenzelm
parents: 56303
diff changeset
    66
            val xml =
61715
5dc95d957569 speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents: 60956
diff changeset
    67
              ML_Name_Space.displayTypeExpression (types, depth, space)
62663
bea354f6ff21 clarified modules;
wenzelm
parents: 62516
diff changeset
    68
              |> Pretty.from_polyml |> Pretty.string_of
56304
40274e4f5ebf redirect ML_Compiler reports more directly: only the (big) parse tree report is deferred via Execution.print (NB: this does not work for asynchronous "diag" commands);
wenzelm
parents: 56303
diff changeset
    69
              |> Output.output |> YXML.parse_body;
40274e4f5ebf redirect ML_Compiler reports more directly: only the (big) parse tree report is deferred via Execution.print (NB: this does not work for asynchronous "diag" commands);
wenzelm
parents: 56303
diff changeset
    70
          in cons (pos, fn () => Markup.ML_typing, fn () => YXML.string_of_body xml) end
40274e4f5ebf redirect ML_Compiler reports more directly: only the (big) parse tree report is deferred via Execution.print (NB: this does not work for asynchronous "diag" commands);
wenzelm
parents: 56303
diff changeset
    71
      end;
38720
7f8bc335e203 ML_Context.eval: produce antiquotation environment preferably in invisible context, to avoid displaced report messages from ML_Compiler;
wenzelm
parents: 38228
diff changeset
    72
44737
03a5ba7213cf bulk reports for improved message throughput;
wenzelm
parents: 43710
diff changeset
    73
    fun reported_entity kind loc decl =
58991
92b6f4e68c5a more careful ML source positions, for improved PIDE markup;
wenzelm
parents: 56618
diff changeset
    74
      let
62516
5732f1c31566 tuned signature -- clarified modules;
wenzelm
parents: 62505
diff changeset
    75
        val pos = Exn_Properties.position_of_location loc;
5732f1c31566 tuned signature -- clarified modules;
wenzelm
parents: 62505
diff changeset
    76
        val def_pos = Exn_Properties.position_of_location decl;
58991
92b6f4e68c5a more careful ML source positions, for improved PIDE markup;
wenzelm
parents: 56618
diff changeset
    77
      in
92b6f4e68c5a more careful ML source positions, for improved PIDE markup;
wenzelm
parents: 56618
diff changeset
    78
        (is_reported pos andalso pos <> def_pos) ?
56304
40274e4f5ebf redirect ML_Compiler reports more directly: only the (big) parse tree report is deferred via Execution.print (NB: this does not work for asynchronous "diag" commands);
wenzelm
parents: 56303
diff changeset
    79
          let
40274e4f5ebf redirect ML_Compiler reports more directly: only the (big) parse tree report is deferred via Execution.print (NB: this does not work for asynchronous "diag" commands);
wenzelm
parents: 56303
diff changeset
    80
            fun markup () =
40274e4f5ebf redirect ML_Compiler reports more directly: only the (big) parse tree report is deferred via Execution.print (NB: this does not work for asynchronous "diag" commands);
wenzelm
parents: 56303
diff changeset
    81
              (Markup.entityN, (Markup.kindN, kind) :: Position.def_properties_of def_pos);
40274e4f5ebf redirect ML_Compiler reports more directly: only the (big) parse tree report is deferred via Execution.print (NB: this does not work for asynchronous "diag" commands);
wenzelm
parents: 56303
diff changeset
    82
          in cons (pos, markup, fn () => "") end
40274e4f5ebf redirect ML_Compiler reports more directly: only the (big) parse tree report is deferred via Execution.print (NB: this does not work for asynchronous "diag" commands);
wenzelm
parents: 56303
diff changeset
    83
      end;
41503
a7462e442e35 refined report_parse_tree: reverse reports happen to produce proper type information for inlined @{term}, @{typ} etc.;
wenzelm
parents: 41501
diff changeset
    84
60731
4ac4b314d93c additional ML parse tree components for Poly/ML 5.5.3, or later;
wenzelm
parents: 60730
diff changeset
    85
    fun reported_completions loc names =
62516
5732f1c31566 tuned signature -- clarified modules;
wenzelm
parents: 62505
diff changeset
    86
      let val pos = Exn_Properties.position_of_location loc in
60732
18299765542e clarified boundary cases of completion;
wenzelm
parents: 60731
diff changeset
    87
        if is_reported pos andalso not (null names) then
60731
4ac4b314d93c additional ML parse tree components for Poly/ML 5.5.3, or later;
wenzelm
parents: 60730
diff changeset
    88
          let
60732
18299765542e clarified boundary cases of completion;
wenzelm
parents: 60731
diff changeset
    89
            val completion = Completion.names pos (map (fn a => (a, ("ML", a))) names);
60731
4ac4b314d93c additional ML parse tree components for Poly/ML 5.5.3, or later;
wenzelm
parents: 60730
diff changeset
    90
            val xml = Completion.encode completion;
4ac4b314d93c additional ML parse tree components for Poly/ML 5.5.3, or later;
wenzelm
parents: 60730
diff changeset
    91
          in cons (pos, fn () => Markup.completion, fn () => YXML.string_of_body xml) end
4ac4b314d93c additional ML parse tree components for Poly/ML 5.5.3, or later;
wenzelm
parents: 60730
diff changeset
    92
        else I
4ac4b314d93c additional ML parse tree components for Poly/ML 5.5.3, or later;
wenzelm
parents: 60730
diff changeset
    93
      end;
4ac4b314d93c additional ML parse tree components for Poly/ML 5.5.3, or later;
wenzelm
parents: 60730
diff changeset
    94
60744
4eba53a0ac3d report possible breakpoint positions;
wenzelm
parents: 60732
diff changeset
    95
    fun reported _ (PolyML.PTnextSibling tree) = reported_tree (tree ())
4eba53a0ac3d report possible breakpoint positions;
wenzelm
parents: 60732
diff changeset
    96
      | reported _ (PolyML.PTfirstChild tree) = reported_tree (tree ())
4eba53a0ac3d report possible breakpoint positions;
wenzelm
parents: 60732
diff changeset
    97
      | reported loc (PolyML.PTtype types) = reported_types loc types
56304
40274e4f5ebf redirect ML_Compiler reports more directly: only the (big) parse tree report is deferred via Execution.print (NB: this does not work for asynchronous "diag" commands);
wenzelm
parents: 56303
diff changeset
    98
      | reported loc (PolyML.PTdeclaredAt decl) = reported_entity Markup.ML_defN loc decl
40274e4f5ebf redirect ML_Compiler reports more directly: only the (big) parse tree report is deferred via Execution.print (NB: this does not work for asynchronous "diag" commands);
wenzelm
parents: 56303
diff changeset
    99
      | reported loc (PolyML.PTopenedAt decl) = reported_entity Markup.ML_openN loc decl
40274e4f5ebf redirect ML_Compiler reports more directly: only the (big) parse tree report is deferred via Execution.print (NB: this does not work for asynchronous "diag" commands);
wenzelm
parents: 56303
diff changeset
   100
      | reported loc (PolyML.PTstructureAt decl) = reported_entity Markup.ML_structureN loc decl
62501
98fa1f9a292f discontinued polyml-5.3.0;
wenzelm
parents: 62495
diff changeset
   101
      | reported loc (PolyML.PTcompletions names) = reported_completions loc names
98fa1f9a292f discontinued polyml-5.3.0;
wenzelm
parents: 62495
diff changeset
   102
      | reported _ _ = I
44737
03a5ba7213cf bulk reports for improved message throughput;
wenzelm
parents: 43710
diff changeset
   103
    and reported_tree (loc, props) = fold (reported loc) props;
56304
40274e4f5ebf redirect ML_Compiler reports more directly: only the (big) parse tree report is deferred via Execution.print (NB: this does not work for asynchronous "diag" commands);
wenzelm
parents: 56303
diff changeset
   104
40274e4f5ebf redirect ML_Compiler reports more directly: only the (big) parse tree report is deferred via Execution.print (NB: this does not work for asynchronous "diag" commands);
wenzelm
parents: 56303
diff changeset
   105
    val persistent_reports = reported_tree parse_tree [];
40274e4f5ebf redirect ML_Compiler reports more directly: only the (big) parse tree report is deferred via Execution.print (NB: this does not work for asynchronous "diag" commands);
wenzelm
parents: 56303
diff changeset
   106
40274e4f5ebf redirect ML_Compiler reports more directly: only the (big) parse tree report is deferred via Execution.print (NB: this does not work for asynchronous "diag" commands);
wenzelm
parents: 56303
diff changeset
   107
    fun output () =
40274e4f5ebf redirect ML_Compiler reports more directly: only the (big) parse tree report is deferred via Execution.print (NB: this does not work for asynchronous "diag" commands);
wenzelm
parents: 56303
diff changeset
   108
      persistent_reports
40274e4f5ebf redirect ML_Compiler reports more directly: only the (big) parse tree report is deferred via Execution.print (NB: this does not work for asynchronous "diag" commands);
wenzelm
parents: 56303
diff changeset
   109
      |> map (fn (pos, markup, text) => Position.reported_text pos (markup ()) (text ()))
56333
38f1422ef473 support bulk messages consisting of small string segments, which are more healthy to the Poly/ML RTS and might prevent spurious GC crashes such as MTGCProcessMarkPointers::ScanAddressesInObject;
wenzelm
parents: 56305
diff changeset
   110
      |> Output.report;
60744
4eba53a0ac3d report possible breakpoint positions;
wenzelm
parents: 60732
diff changeset
   111
    val _ =
4eba53a0ac3d report possible breakpoint positions;
wenzelm
parents: 60732
diff changeset
   112
      if not (null persistent_reports) andalso redirect andalso Multithreading.enabled ()
4eba53a0ac3d report possible breakpoint positions;
wenzelm
parents: 60732
diff changeset
   113
      then
4eba53a0ac3d report possible breakpoint positions;
wenzelm
parents: 60732
diff changeset
   114
        Execution.print
4eba53a0ac3d report possible breakpoint positions;
wenzelm
parents: 60732
diff changeset
   115
          {name = "ML_Compiler.report", pos = Position.thread_data (), pri = Task_Queue.urgent_pri}
4eba53a0ac3d report possible breakpoint positions;
wenzelm
parents: 60732
diff changeset
   116
          output
4eba53a0ac3d report possible breakpoint positions;
wenzelm
parents: 60732
diff changeset
   117
      else output ();
4eba53a0ac3d report possible breakpoint positions;
wenzelm
parents: 60732
diff changeset
   118
4eba53a0ac3d report possible breakpoint positions;
wenzelm
parents: 60732
diff changeset
   119
4eba53a0ac3d report possible breakpoint positions;
wenzelm
parents: 60732
diff changeset
   120
    (* breakpoints *)
4eba53a0ac3d report possible breakpoint positions;
wenzelm
parents: 60732
diff changeset
   121
4eba53a0ac3d report possible breakpoint positions;
wenzelm
parents: 60732
diff changeset
   122
    fun breakpoints _ (PolyML.PTnextSibling tree) = breakpoints_tree (tree ())
4eba53a0ac3d report possible breakpoint positions;
wenzelm
parents: 60732
diff changeset
   123
      | breakpoints _ (PolyML.PTfirstChild tree) = breakpoints_tree (tree ())
62501
98fa1f9a292f discontinued polyml-5.3.0;
wenzelm
parents: 62495
diff changeset
   124
      | breakpoints loc (PolyML.PTbreakPoint b) =
98fa1f9a292f discontinued polyml-5.3.0;
wenzelm
parents: 62495
diff changeset
   125
          let val pos = breakpoint_position loc in
98fa1f9a292f discontinued polyml-5.3.0;
wenzelm
parents: 62495
diff changeset
   126
            if is_reported pos then
98fa1f9a292f discontinued polyml-5.3.0;
wenzelm
parents: 62495
diff changeset
   127
              let val id = serial ();
98fa1f9a292f discontinued polyml-5.3.0;
wenzelm
parents: 62495
diff changeset
   128
              in cons ((pos, Markup.ML_breakpoint id), (id, (b, pos))) end
98fa1f9a292f discontinued polyml-5.3.0;
wenzelm
parents: 62495
diff changeset
   129
            else I
98fa1f9a292f discontinued polyml-5.3.0;
wenzelm
parents: 62495
diff changeset
   130
          end
98fa1f9a292f discontinued polyml-5.3.0;
wenzelm
parents: 62495
diff changeset
   131
      | breakpoints _ _ = I
60744
4eba53a0ac3d report possible breakpoint positions;
wenzelm
parents: 60732
diff changeset
   132
    and breakpoints_tree (loc, props) = fold (breakpoints loc) props;
4eba53a0ac3d report possible breakpoint positions;
wenzelm
parents: 60732
diff changeset
   133
4eba53a0ac3d report possible breakpoint positions;
wenzelm
parents: 60732
diff changeset
   134
    val all_breakpoints = rev (breakpoints_tree parse_tree []);
4eba53a0ac3d report possible breakpoint positions;
wenzelm
parents: 60732
diff changeset
   135
    val _ = Position.reports (map #1 all_breakpoints);
60746
8cf877aca29a store breakpoints within ML environment;
wenzelm
parents: 60745
diff changeset
   136
    val _ =
8cf877aca29a store breakpoints within ML environment;
wenzelm
parents: 60745
diff changeset
   137
      if is_some (Context.thread_data ()) then
8cf877aca29a store breakpoints within ML environment;
wenzelm
parents: 60745
diff changeset
   138
        Context.>> (fold (ML_Env.add_breakpoint o #2) all_breakpoints)
8cf877aca29a store breakpoints within ML environment;
wenzelm
parents: 60745
diff changeset
   139
      else ();
8cf877aca29a store breakpoints within ML environment;
wenzelm
parents: 60745
diff changeset
   140
  in () end;
31333
fcd010617e6c added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff changeset
   141
fcd010617e6c added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff changeset
   142
fcd010617e6c added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff changeset
   143
(* eval ML source tokens *)
fcd010617e6c added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff changeset
   144
56304
40274e4f5ebf redirect ML_Compiler reports more directly: only the (big) parse tree report is deferred via Execution.print (NB: this does not work for asynchronous "diag" commands);
wenzelm
parents: 56303
diff changeset
   145
fun eval (flags: flags) pos toks =
31333
fcd010617e6c added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff changeset
   146
  let
62493
dd154240a53c load secure.ML earlier;
wenzelm
parents: 62490
diff changeset
   147
    val _ = Secure.deny_ml ();
62495
83db706d7771 tuned signature;
wenzelm
parents: 62493
diff changeset
   148
    val space = ML_Env.make_name_space {SML = #SML flags, exchange = #exchange flags};
56265
785569927666 discontinued Toplevel.debug in favour of system option "exception_trace";
wenzelm
parents: 55837
diff changeset
   149
    val opt_context = Context.thread_data ();
31333
fcd010617e6c added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff changeset
   150
fcd010617e6c added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff changeset
   151
fcd010617e6c added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff changeset
   152
    (* input *)
fcd010617e6c added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff changeset
   153
50911
ee7fe4230642 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents: 50910
diff changeset
   154
    val location_props = op ^ (YXML.output_markup (":", #props (Position.dest pos)));
31437
70309dc3deac removed unused location_of;
wenzelm
parents: 31434
diff changeset
   155
59110
8a78c7cb5b14 some special cases for official SML, to treat Isabelle symbols like raw characters;
wenzelm
parents: 58991
diff changeset
   156
    val input_explode =
8a78c7cb5b14 some special cases for official SML, to treat Isabelle symbols like raw characters;
wenzelm
parents: 58991
diff changeset
   157
      if #SML flags then String.explode
8a78c7cb5b14 some special cases for official SML, to treat Isabelle symbols like raw characters;
wenzelm
parents: 58991
diff changeset
   158
      else maps (String.explode o Symbol.esc) o Symbol.explode;
8a78c7cb5b14 some special cases for official SML, to treat Isabelle symbols like raw characters;
wenzelm
parents: 58991
diff changeset
   159
41501
b5ad6b0d6d7c ML compiler: more careful treatment of input tokens -- trailing space ensures proper separation and end position (cf. 82c1e348bc18, 08240feb69c7);
wenzelm
parents: 41484
diff changeset
   160
    val input_buffer =
59110
8a78c7cb5b14 some special cases for official SML, to treat Isabelle symbols like raw characters;
wenzelm
parents: 58991
diff changeset
   161
      Unsynchronized.ref (toks |> map (`(input_explode o ML_Lex.check_content_of)));
31333
fcd010617e6c added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff changeset
   162
fcd010617e6c added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff changeset
   163
    fun get () =
fcd010617e6c added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff changeset
   164
      (case ! input_buffer of
41501
b5ad6b0d6d7c ML compiler: more careful treatment of input tokens -- trailing space ensures proper separation and end position (cf. 82c1e348bc18, 08240feb69c7);
wenzelm
parents: 41484
diff changeset
   165
        (c :: cs, tok) :: rest => (input_buffer := (cs, tok) :: rest; SOME c)
b5ad6b0d6d7c ML compiler: more careful treatment of input tokens -- trailing space ensures proper separation and end position (cf. 82c1e348bc18, 08240feb69c7);
wenzelm
parents: 41484
diff changeset
   166
      | ([], _) :: rest => (input_buffer := rest; SOME #" ")
b5ad6b0d6d7c ML compiler: more careful treatment of input tokens -- trailing space ensures proper separation and end position (cf. 82c1e348bc18, 08240feb69c7);
wenzelm
parents: 41484
diff changeset
   167
      | [] => NONE);
b5ad6b0d6d7c ML compiler: more careful treatment of input tokens -- trailing space ensures proper separation and end position (cf. 82c1e348bc18, 08240feb69c7);
wenzelm
parents: 41484
diff changeset
   168
b5ad6b0d6d7c ML compiler: more careful treatment of input tokens -- trailing space ensures proper separation and end position (cf. 82c1e348bc18, 08240feb69c7);
wenzelm
parents: 41484
diff changeset
   169
    fun get_pos () =
b5ad6b0d6d7c ML compiler: more careful treatment of input tokens -- trailing space ensures proper separation and end position (cf. 82c1e348bc18, 08240feb69c7);
wenzelm
parents: 41484
diff changeset
   170
      (case ! input_buffer of
b5ad6b0d6d7c ML compiler: more careful treatment of input tokens -- trailing space ensures proper separation and end position (cf. 82c1e348bc18, 08240feb69c7);
wenzelm
parents: 41484
diff changeset
   171
        (_ :: _, tok) :: _ => ML_Lex.pos_of tok
b5ad6b0d6d7c ML compiler: more careful treatment of input tokens -- trailing space ensures proper separation and end position (cf. 82c1e348bc18, 08240feb69c7);
wenzelm
parents: 41484
diff changeset
   172
      | ([], tok) :: _ => ML_Lex.end_pos_of tok
b5ad6b0d6d7c ML compiler: more careful treatment of input tokens -- trailing space ensures proper separation and end position (cf. 82c1e348bc18, 08240feb69c7);
wenzelm
parents: 41484
diff changeset
   173
      | [] => Position.none);
31333
fcd010617e6c added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff changeset
   174
fcd010617e6c added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff changeset
   175
60744
4eba53a0ac3d report possible breakpoint positions;
wenzelm
parents: 60732
diff changeset
   176
    (* output *)
39228
cb7264721c91 ML_Compiler.eval: more careful printing of messages and regular output, trying to accomodate Poly/ML, Proof General, Isabelle/Scala/jEdit at the same time;
wenzelm
parents: 39227
diff changeset
   177
cb7264721c91 ML_Compiler.eval: more careful printing of messages and regular output, trying to accomodate Poly/ML, Proof General, Isabelle/Scala/jEdit at the same time;
wenzelm
parents: 39227
diff changeset
   178
    val writeln_buffer = Unsynchronized.ref Buffer.empty;
cb7264721c91 ML_Compiler.eval: more careful printing of messages and regular output, trying to accomodate Poly/ML, Proof General, Isabelle/Scala/jEdit at the same time;
wenzelm
parents: 39227
diff changeset
   179
    fun write s = Unsynchronized.change writeln_buffer (Buffer.add s);
60858
7bf2188a0998 evaluate ML expressions within debugger context;
wenzelm
parents: 60746
diff changeset
   180
    fun output_writeln () = #writeln flags (trim_line (Buffer.content (! writeln_buffer)));
39228
cb7264721c91 ML_Compiler.eval: more careful printing of messages and regular output, trying to accomodate Poly/ML, Proof General, Isabelle/Scala/jEdit at the same time;
wenzelm
parents: 39227
diff changeset
   181
cb7264721c91 ML_Compiler.eval: more careful printing of messages and regular output, trying to accomodate Poly/ML, Proof General, Isabelle/Scala/jEdit at the same time;
wenzelm
parents: 39227
diff changeset
   182
    val warnings = Unsynchronized.ref ([]: string list);
39231
25c345302a17 avoid mixing of static and runtime errors in compiler output, to accomodate Proof General;
wenzelm
parents: 39230
diff changeset
   183
    fun warn msg = Unsynchronized.change warnings (cons msg);
60858
7bf2188a0998 evaluate ML expressions within debugger context;
wenzelm
parents: 60746
diff changeset
   184
    fun output_warnings () = List.app (#warning flags) (rev (! warnings));
39228
cb7264721c91 ML_Compiler.eval: more careful printing of messages and regular output, trying to accomodate Poly/ML, Proof General, Isabelle/Scala/jEdit at the same time;
wenzelm
parents: 39227
diff changeset
   185
cb7264721c91 ML_Compiler.eval: more careful printing of messages and regular output, trying to accomodate Poly/ML, Proof General, Isabelle/Scala/jEdit at the same time;
wenzelm
parents: 39227
diff changeset
   186
    val error_buffer = Unsynchronized.ref Buffer.empty;
39231
25c345302a17 avoid mixing of static and runtime errors in compiler output, to accomodate Proof General;
wenzelm
parents: 39230
diff changeset
   187
    fun err msg = Unsynchronized.change error_buffer (Buffer.add msg #> Buffer.add "\n");
60872
9f45c2f1cbfd tuned messages;
wenzelm
parents: 60858
diff changeset
   188
    fun flush_error () = #writeln flags (trim_line (Buffer.content (! error_buffer)));
9f45c2f1cbfd tuned messages;
wenzelm
parents: 60858
diff changeset
   189
    fun raise_error msg = error (trim_line (Buffer.content (Buffer.add msg (! error_buffer))));
31333
fcd010617e6c added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff changeset
   190
39228
cb7264721c91 ML_Compiler.eval: more careful printing of messages and regular output, trying to accomodate Poly/ML, Proof General, Isabelle/Scala/jEdit at the same time;
wenzelm
parents: 39227
diff changeset
   191
    fun message {message = msg, hard, location = loc, context = _} =
cb7264721c91 ML_Compiler.eval: more careful printing of messages and regular output, trying to accomodate Poly/ML, Proof General, Isabelle/Scala/jEdit at the same time;
wenzelm
parents: 39227
diff changeset
   192
      let
62516
5732f1c31566 tuned signature -- clarified modules;
wenzelm
parents: 62505
diff changeset
   193
        val pos = Exn_Properties.position_of_location loc;
39228
cb7264721c91 ML_Compiler.eval: more careful printing of messages and regular output, trying to accomodate Poly/ML, Proof General, Isabelle/Scala/jEdit at the same time;
wenzelm
parents: 39227
diff changeset
   194
        val txt =
49828
5631ee099293 more basic ML compiler messages -- avoid conflict of 638cefe3ee99 and cb7264721c91 concerning Protocol.message_positions;
wenzelm
parents: 48992
diff changeset
   195
          (if hard then "ML error" else "ML warning") ^ Position.here pos ^ ":\n" ^
62663
bea354f6ff21 clarified modules;
wenzelm
parents: 62516
diff changeset
   196
          Pretty.string_of (Pretty.from_polyml msg);
39231
25c345302a17 avoid mixing of static and runtime errors in compiler output, to accomodate Proof General;
wenzelm
parents: 39230
diff changeset
   197
      in if hard then err txt else warn txt end;
31333
fcd010617e6c added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff changeset
   198
fcd010617e6c added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff changeset
   199
fcd010617e6c added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff changeset
   200
    (* results *)
fcd010617e6c added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff changeset
   201
62387
ad3eb2889f9a support for polyml-git ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents: 62357
diff changeset
   202
    val depth = FixedInt.fromInt (ML_Options.get_print_depth ());
31333
fcd010617e6c added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff changeset
   203
fcd010617e6c added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff changeset
   204
    fun apply_result {fixes, types, signatures, structures, functors, values} =
fcd010617e6c added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff changeset
   205
      let
fcd010617e6c added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff changeset
   206
        fun display disp x =
fcd010617e6c added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff changeset
   207
          if depth > 0 then
62663
bea354f6ff21 clarified modules;
wenzelm
parents: 62516
diff changeset
   208
            (write (disp x |> Pretty.from_polyml |> Pretty.string_of); write "\n")
31333
fcd010617e6c added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff changeset
   209
          else ();
fcd010617e6c added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff changeset
   210
fcd010617e6c added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff changeset
   211
        fun apply_fix (a, b) =
61715
5dc95d957569 speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents: 60956
diff changeset
   212
          (#enterFix space (a, b); display ML_Name_Space.displayFix (a, b));
31333
fcd010617e6c added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff changeset
   213
        fun apply_type (a, b) =
61715
5dc95d957569 speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents: 60956
diff changeset
   214
          (#enterType space (a, b); display ML_Name_Space.displayType (b, depth, space));
31333
fcd010617e6c added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff changeset
   215
        fun apply_sig (a, b) =
61715
5dc95d957569 speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents: 60956
diff changeset
   216
          (#enterSig space (a, b); display ML_Name_Space.displaySig (b, depth, space));
31333
fcd010617e6c added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff changeset
   217
        fun apply_struct (a, b) =
61715
5dc95d957569 speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents: 60956
diff changeset
   218
          (#enterStruct space (a, b); display ML_Name_Space.displayStruct (b, depth, space));
31333
fcd010617e6c added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff changeset
   219
        fun apply_funct (a, b) =
61715
5dc95d957569 speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents: 60956
diff changeset
   220
          (#enterFunct space (a, b); display ML_Name_Space.displayFunct (b, depth, space));
31333
fcd010617e6c added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff changeset
   221
        fun apply_val (a, b) =
61715
5dc95d957569 speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents: 60956
diff changeset
   222
          (#enterVal space (a, b); display ML_Name_Space.displayVal (b, depth, space));
31333
fcd010617e6c added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff changeset
   223
      in
fcd010617e6c added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff changeset
   224
        List.app apply_fix fixes;
fcd010617e6c added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff changeset
   225
        List.app apply_type types;
fcd010617e6c added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff changeset
   226
        List.app apply_sig signatures;
fcd010617e6c added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff changeset
   227
        List.app apply_struct structures;
fcd010617e6c added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff changeset
   228
        List.app apply_funct functors;
fcd010617e6c added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff changeset
   229
        List.app apply_val values
fcd010617e6c added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff changeset
   230
      end;
fcd010617e6c added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff changeset
   231
39231
25c345302a17 avoid mixing of static and runtime errors in compiler output, to accomodate Proof General;
wenzelm
parents: 39230
diff changeset
   232
    exception STATIC_ERRORS of unit;
39230
184507f6e8d0 ML_Compiler.eval: discontinued extra "Static Errors" of raw Poly/ML;
wenzelm
parents: 39228
diff changeset
   233
31333
fcd010617e6c added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff changeset
   234
    fun result_fun (phase1, phase2) () =
31477
ae1a00e1a2f6 added exn_message (formerly in toplevel.ML);
wenzelm
parents: 31475
diff changeset
   235
     ((case phase1 of
ae1a00e1a2f6 added exn_message (formerly in toplevel.ML);
wenzelm
parents: 31475
diff changeset
   236
        NONE => ()
60746
8cf877aca29a store breakpoints within ML environment;
wenzelm
parents: 60745
diff changeset
   237
      | SOME parse_tree => report_parse_tree (#redirect flags) depth space parse_tree);
31477
ae1a00e1a2f6 added exn_message (formerly in toplevel.ML);
wenzelm
parents: 31475
diff changeset
   238
      (case phase2 of
39231
25c345302a17 avoid mixing of static and runtime errors in compiler output, to accomodate Proof General;
wenzelm
parents: 39230
diff changeset
   239
        NONE => raise STATIC_ERRORS ()
31477
ae1a00e1a2f6 added exn_message (formerly in toplevel.ML);
wenzelm
parents: 31475
diff changeset
   240
      | SOME code =>
33603
3713a5208671 generalized Runtime.toplevel_error wrt. output function;
wenzelm
parents: 33538
diff changeset
   241
          apply_result
3713a5208671 generalized Runtime.toplevel_error wrt. output function;
wenzelm
parents: 33538
diff changeset
   242
            ((code
56303
4cc3f4db3447 clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents: 56281
diff changeset
   243
              |> Runtime.debugging opt_context
4cc3f4db3447 clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents: 56281
diff changeset
   244
              |> Runtime.toplevel_error (err o Runtime.exn_message)) ())));
31333
fcd010617e6c added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff changeset
   245
fcd010617e6c added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff changeset
   246
fcd010617e6c added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff changeset
   247
    (* compiler invocation *)
fcd010617e6c added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff changeset
   248
60956
10d463883dc2 explicit debug flag for ML compiler;
wenzelm
parents: 60913
diff changeset
   249
    val debug =
10d463883dc2 explicit debug flag for ML compiler;
wenzelm
parents: 60913
diff changeset
   250
      (case #debug flags of
10d463883dc2 explicit debug flag for ML compiler;
wenzelm
parents: 60913
diff changeset
   251
        SOME debug => debug
10d463883dc2 explicit debug flag for ML compiler;
wenzelm
parents: 60913
diff changeset
   252
      | NONE => ML_Options.debugger_enabled opt_context);
10d463883dc2 explicit debug flag for ML compiler;
wenzelm
parents: 60913
diff changeset
   253
31333
fcd010617e6c added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff changeset
   254
    val parameters =
39228
cb7264721c91 ML_Compiler.eval: more careful printing of messages and regular output, trying to accomodate Poly/ML, Proof General, Isabelle/Scala/jEdit at the same time;
wenzelm
parents: 39227
diff changeset
   255
     [PolyML.Compiler.CPOutStream write,
31333
fcd010617e6c added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff changeset
   256
      PolyML.Compiler.CPNameSpace space,
39228
cb7264721c91 ML_Compiler.eval: more careful printing of messages and regular output, trying to accomodate Poly/ML, Proof General, Isabelle/Scala/jEdit at the same time;
wenzelm
parents: 39227
diff changeset
   257
      PolyML.Compiler.CPErrorMessageProc message,
41501
b5ad6b0d6d7c ML compiler: more careful treatment of input tokens -- trailing space ensures proper separation and end position (cf. 82c1e348bc18, 08240feb69c7);
wenzelm
parents: 41484
diff changeset
   258
      PolyML.Compiler.CPLineNo (the_default 0 o Position.line_of o get_pos),
b5ad6b0d6d7c ML compiler: more careful treatment of input tokens -- trailing space ensures proper separation and end position (cf. 82c1e348bc18, 08240feb69c7);
wenzelm
parents: 41484
diff changeset
   259
      PolyML.Compiler.CPLineOffset (the_default 0 o Position.offset_of o get_pos),
31437
70309dc3deac removed unused location_of;
wenzelm
parents: 31434
diff changeset
   260
      PolyML.Compiler.CPFileName location_props,
56303
4cc3f4db3447 clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents: 56281
diff changeset
   261
      PolyML.Compiler.CPPrintDepth ML_Options.get_print_depth,
31475
85e864045497 report_parse_tree: ML_open, ML_struct;
wenzelm
parents: 31437
diff changeset
   262
      PolyML.Compiler.CPCompilerResultFun result_fun,
62501
98fa1f9a292f discontinued polyml-5.3.0;
wenzelm
parents: 62495
diff changeset
   263
      PolyML.Compiler.CPPrintInAlphabeticalOrder false,
98fa1f9a292f discontinued polyml-5.3.0;
wenzelm
parents: 62495
diff changeset
   264
      PolyML.Compiler.CPDebug debug];
60956
10d463883dc2 explicit debug flag for ML compiler;
wenzelm
parents: 60913
diff changeset
   265
31333
fcd010617e6c added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff changeset
   266
    val _ =
fcd010617e6c added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff changeset
   267
      (while not (List.null (! input_buffer)) do
fcd010617e6c added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff changeset
   268
        PolyML.compiler (get, parameters) ())
39232
69c6d3e87660 more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents: 39231
diff changeset
   269
      handle exn =>
62505
9e2a65912111 clarified modules;
wenzelm
parents: 62503
diff changeset
   270
        if Exn.is_interrupt exn then Exn.reraise exn
39232
69c6d3e87660 more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents: 39231
diff changeset
   271
        else
69c6d3e87660 more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents: 39231
diff changeset
   272
          let
69c6d3e87660 more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents: 39231
diff changeset
   273
            val exn_msg =
69c6d3e87660 more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents: 39231
diff changeset
   274
              (case exn of
69c6d3e87660 more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents: 39231
diff changeset
   275
                STATIC_ERRORS () => ""
69c6d3e87660 more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents: 39231
diff changeset
   276
              | Runtime.TOPLEVEL_ERROR => ""
62516
5732f1c31566 tuned signature -- clarified modules;
wenzelm
parents: 62505
diff changeset
   277
              | _ => "Exception- " ^ Pretty.string_of (Runtime.pretty_exn exn) ^ " raised");
39232
69c6d3e87660 more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents: 39231
diff changeset
   278
            val _ = output_warnings ();
69c6d3e87660 more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents: 39231
diff changeset
   279
            val _ = output_writeln ();
69c6d3e87660 more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents: 39231
diff changeset
   280
          in raise_error exn_msg end;
39228
cb7264721c91 ML_Compiler.eval: more careful printing of messages and regular output, trying to accomodate Poly/ML, Proof General, Isabelle/Scala/jEdit at the same time;
wenzelm
parents: 39227
diff changeset
   281
  in
56304
40274e4f5ebf redirect ML_Compiler reports more directly: only the (big) parse tree report is deferred via Execution.print (NB: this does not work for asynchronous "diag" commands);
wenzelm
parents: 56303
diff changeset
   282
    if #verbose flags then (output_warnings (); flush_error (); output_writeln ())
39228
cb7264721c91 ML_Compiler.eval: more careful printing of messages and regular output, trying to accomodate Poly/ML, Proof General, Isabelle/Scala/jEdit at the same time;
wenzelm
parents: 39227
diff changeset
   283
    else ()
cb7264721c91 ML_Compiler.eval: more careful printing of messages and regular output, trying to accomodate Poly/ML, Proof General, Isabelle/Scala/jEdit at the same time;
wenzelm
parents: 39227
diff changeset
   284
  end;
31333
fcd010617e6c added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff changeset
   285
fcd010617e6c added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff changeset
   286
end;