src/Pure/ML/ml_test.ML
author wenzelm
Tue, 24 Mar 2009 16:11:09 +0100
changeset 30705 e8ab35c6ade6
parent 30704 d6d4828e74a2
child 30709 d9ca766bf24c
permissions -rw-r--r--
get_index: produce index of next pending token, not the last one;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
30640
3f3d1e218b64 Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/ML/ml_test.ML
3f3d1e218b64 Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
3f3d1e218b64 Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff changeset
     3
3f3d1e218b64 Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff changeset
     4
Test of advanced ML compiler invocation in Poly/ML 5.3.
3f3d1e218b64 Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff changeset
     5
*)
3f3d1e218b64 Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff changeset
     6
30646
d26ad4576d5c proper signature;
wenzelm
parents: 30644
diff changeset
     7
signature ML_TEST =
d26ad4576d5c proper signature;
wenzelm
parents: 30644
diff changeset
     8
sig
30680
0863bb353065 more systematic type use_context;
wenzelm
parents: 30677
diff changeset
     9
  val eval: bool -> Position.T -> ML_Lex.token list -> unit
30646
d26ad4576d5c proper signature;
wenzelm
parents: 30644
diff changeset
    10
end
d26ad4576d5c proper signature;
wenzelm
parents: 30644
diff changeset
    11
d26ad4576d5c proper signature;
wenzelm
parents: 30644
diff changeset
    12
structure ML_Test: ML_TEST =
30640
3f3d1e218b64 Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff changeset
    13
struct
3f3d1e218b64 Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff changeset
    14
30704
d6d4828e74a2 register token positions persistently with context;
wenzelm
parents: 30681
diff changeset
    15
(* extra ML environment *)
30640
3f3d1e218b64 Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff changeset
    16
30704
d6d4828e74a2 register token positions persistently with context;
wenzelm
parents: 30681
diff changeset
    17
structure Extra_Env = GenericDataFun
30646
d26ad4576d5c proper signature;
wenzelm
parents: 30644
diff changeset
    18
(
30704
d6d4828e74a2 register token positions persistently with context;
wenzelm
parents: 30681
diff changeset
    19
  type T = Position.T Inttab.table;  (*position of registered tokens*)
d6d4828e74a2 register token positions persistently with context;
wenzelm
parents: 30681
diff changeset
    20
  val empty = Inttab.empty;
d6d4828e74a2 register token positions persistently with context;
wenzelm
parents: 30681
diff changeset
    21
  val extend = I;
d6d4828e74a2 register token positions persistently with context;
wenzelm
parents: 30681
diff changeset
    22
  fun merge _ = Inttab.merge (K true);
30646
d26ad4576d5c proper signature;
wenzelm
parents: 30644
diff changeset
    23
);
d26ad4576d5c proper signature;
wenzelm
parents: 30644
diff changeset
    24
30704
d6d4828e74a2 register token positions persistently with context;
wenzelm
parents: 30681
diff changeset
    25
fun inherit_env context =
d6d4828e74a2 register token positions persistently with context;
wenzelm
parents: 30681
diff changeset
    26
  ML_Context.inherit_env context #>
d6d4828e74a2 register token positions persistently with context;
wenzelm
parents: 30681
diff changeset
    27
  Extra_Env.put (Extra_Env.get context);
d6d4828e74a2 register token positions persistently with context;
wenzelm
parents: 30681
diff changeset
    28
d6d4828e74a2 register token positions persistently with context;
wenzelm
parents: 30681
diff changeset
    29
fun register_tokens toks context =
d6d4828e74a2 register token positions persistently with context;
wenzelm
parents: 30681
diff changeset
    30
  let
d6d4828e74a2 register token positions persistently with context;
wenzelm
parents: 30681
diff changeset
    31
    val regs = map (fn tok => (serial (), tok)) toks;
d6d4828e74a2 register token positions persistently with context;
wenzelm
parents: 30681
diff changeset
    32
    val context' = context
d6d4828e74a2 register token positions persistently with context;
wenzelm
parents: 30681
diff changeset
    33
      |> Extra_Env.map (fold (fn (i, tok) => Inttab.update (i, ML_Lex.pos_of tok)) regs);
d6d4828e74a2 register token positions persistently with context;
wenzelm
parents: 30681
diff changeset
    34
  in (regs, context') end;
d6d4828e74a2 register token positions persistently with context;
wenzelm
parents: 30681
diff changeset
    35
d6d4828e74a2 register token positions persistently with context;
wenzelm
parents: 30681
diff changeset
    36
fun pos_of_location context
d6d4828e74a2 register token positions persistently with context;
wenzelm
parents: 30681
diff changeset
    37
    ({file, startLine = line, startPosition = i, endPosition = j, ...}: location) =
d6d4828e74a2 register token positions persistently with context;
wenzelm
parents: 30681
diff changeset
    38
  (case pairself (Inttab.lookup (Extra_Env.get context)) (i, j) of
d6d4828e74a2 register token positions persistently with context;
wenzelm
parents: 30681
diff changeset
    39
    (SOME pos1, SOME pos2) => Position.encode_range (pos1, pos2)
d6d4828e74a2 register token positions persistently with context;
wenzelm
parents: 30681
diff changeset
    40
  | (SOME pos, NONE) => pos
d6d4828e74a2 register token positions persistently with context;
wenzelm
parents: 30681
diff changeset
    41
  | _ => Position.line_file line file);
d6d4828e74a2 register token positions persistently with context;
wenzelm
parents: 30681
diff changeset
    42
30646
d26ad4576d5c proper signature;
wenzelm
parents: 30644
diff changeset
    43
30704
d6d4828e74a2 register token positions persistently with context;
wenzelm
parents: 30681
diff changeset
    44
(* parse trees *)
d6d4828e74a2 register token positions persistently with context;
wenzelm
parents: 30681
diff changeset
    45
d6d4828e74a2 register token positions persistently with context;
wenzelm
parents: 30681
diff changeset
    46
fun report_parse_tree context =
d6d4828e74a2 register token positions persistently with context;
wenzelm
parents: 30681
diff changeset
    47
  let
d6d4828e74a2 register token positions persistently with context;
wenzelm
parents: 30681
diff changeset
    48
    val pos_of = pos_of_location context;
d6d4828e74a2 register token positions persistently with context;
wenzelm
parents: 30681
diff changeset
    49
    fun report loc (PTtype types) =  (* FIXME body text *)
d6d4828e74a2 register token positions persistently with context;
wenzelm
parents: 30681
diff changeset
    50
          Position.report Markup.ML_typing (pos_of loc)
d6d4828e74a2 register token positions persistently with context;
wenzelm
parents: 30681
diff changeset
    51
      | report loc (PTdeclaredAt decl) =
d6d4828e74a2 register token positions persistently with context;
wenzelm
parents: 30681
diff changeset
    52
          Markup.markup (Markup.properties (Position.properties_of (pos_of decl)) Markup.ML_def) ""
d6d4828e74a2 register token positions persistently with context;
wenzelm
parents: 30681
diff changeset
    53
          |> Position.report_text Markup.ML_ref (pos_of loc)
d6d4828e74a2 register token positions persistently with context;
wenzelm
parents: 30681
diff changeset
    54
      | report _ (PTnextSibling tree) = report_tree (tree ())
d6d4828e74a2 register token positions persistently with context;
wenzelm
parents: 30681
diff changeset
    55
      | report _ (PTfirstChild tree) = report_tree (tree ())
d6d4828e74a2 register token positions persistently with context;
wenzelm
parents: 30681
diff changeset
    56
      | report _ _ = ()
d6d4828e74a2 register token positions persistently with context;
wenzelm
parents: 30681
diff changeset
    57
    and report_tree (loc, props) = List.app (report loc) props;
d6d4828e74a2 register token positions persistently with context;
wenzelm
parents: 30681
diff changeset
    58
  in report_tree end;
d6d4828e74a2 register token positions persistently with context;
wenzelm
parents: 30681
diff changeset
    59
d6d4828e74a2 register token positions persistently with context;
wenzelm
parents: 30681
diff changeset
    60
d6d4828e74a2 register token positions persistently with context;
wenzelm
parents: 30681
diff changeset
    61
(* eval ML source tokens *)
30680
0863bb353065 more systematic type use_context;
wenzelm
parents: 30677
diff changeset
    62
0863bb353065 more systematic type use_context;
wenzelm
parents: 30677
diff changeset
    63
fun use_text ({name_space = space, print, error, ...}: use_context) verbose pos toks =
30640
3f3d1e218b64 Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff changeset
    64
  let
30680
0863bb353065 more systematic type use_context;
wenzelm
parents: 30677
diff changeset
    65
    (* input *)
0863bb353065 more systematic type use_context;
wenzelm
parents: 30677
diff changeset
    66
30704
d6d4828e74a2 register token positions persistently with context;
wenzelm
parents: 30681
diff changeset
    67
    val input = Context.>>> (register_tokens toks);
d6d4828e74a2 register token positions persistently with context;
wenzelm
parents: 30681
diff changeset
    68
    val input_buffer = ref (map (apsnd (String.explode o ML_Lex.text_of)) input);
d6d4828e74a2 register token positions persistently with context;
wenzelm
parents: 30681
diff changeset
    69
d6d4828e74a2 register token positions persistently with context;
wenzelm
parents: 30681
diff changeset
    70
    val current_line = ref (the_default 1 (Position.line_of pos));
30640
3f3d1e218b64 Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff changeset
    71
30705
e8ab35c6ade6 get_index: produce index of next pending token, not the last one;
wenzelm
parents: 30704
diff changeset
    72
    fun get_index () =
e8ab35c6ade6 get_index: produce index of next pending token, not the last one;
wenzelm
parents: 30704
diff changeset
    73
      the_default 0 (get_first (fn (_, []) => NONE | (i, _) => SOME i) (! input_buffer));
e8ab35c6ade6 get_index: produce index of next pending token, not the last one;
wenzelm
parents: 30704
diff changeset
    74
30640
3f3d1e218b64 Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff changeset
    75
    fun get () =
30704
d6d4828e74a2 register token positions persistently with context;
wenzelm
parents: 30681
diff changeset
    76
      (case ! input_buffer of
30640
3f3d1e218b64 Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff changeset
    77
        [] => NONE
30704
d6d4828e74a2 register token positions persistently with context;
wenzelm
parents: 30681
diff changeset
    78
      | (_, []) :: rest => (input_buffer := rest; get ())
30640
3f3d1e218b64 Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff changeset
    79
      | (i, c :: cs) :: rest =>
30704
d6d4828e74a2 register token positions persistently with context;
wenzelm
parents: 30681
diff changeset
    80
          (input_buffer := (i, cs) :: rest;
30640
3f3d1e218b64 Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff changeset
    81
           if c = #"\n" then current_line := ! current_line + 1 else ();
3f3d1e218b64 Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff changeset
    82
           SOME c));
3f3d1e218b64 Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff changeset
    83
30680
0863bb353065 more systematic type use_context;
wenzelm
parents: 30677
diff changeset
    84
0863bb353065 more systematic type use_context;
wenzelm
parents: 30677
diff changeset
    85
    (* output *)
0863bb353065 more systematic type use_context;
wenzelm
parents: 30677
diff changeset
    86
30704
d6d4828e74a2 register token positions persistently with context;
wenzelm
parents: 30681
diff changeset
    87
    val output_buffer = ref Buffer.empty;
d6d4828e74a2 register token positions persistently with context;
wenzelm
parents: 30681
diff changeset
    88
    fun output () = Buffer.content (! output_buffer);
d6d4828e74a2 register token positions persistently with context;
wenzelm
parents: 30681
diff changeset
    89
    fun put s = change output_buffer (Buffer.add s);
30640
3f3d1e218b64 Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff changeset
    90
3f3d1e218b64 Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff changeset
    91
    fun put_message {message, hard, location, context = _} =
3f3d1e218b64 Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff changeset
    92
     (put (if hard then "Error: " else "Warning: ");
3f3d1e218b64 Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff changeset
    93
      put (Pretty.string_of (Pretty.from_ML (pretty_ml message)));
30704
d6d4828e74a2 register token positions persistently with context;
wenzelm
parents: 30681
diff changeset
    94
      put (Position.str_of (pos_of_location (the (Context.thread_data ())) location) ^ "\n"));
30640
3f3d1e218b64 Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff changeset
    95
30680
0863bb353065 more systematic type use_context;
wenzelm
parents: 30677
diff changeset
    96
0863bb353065 more systematic type use_context;
wenzelm
parents: 30677
diff changeset
    97
    (* results *)
0863bb353065 more systematic type use_context;
wenzelm
parents: 30677
diff changeset
    98
0863bb353065 more systematic type use_context;
wenzelm
parents: 30677
diff changeset
    99
    fun apply_result {fixes, types, signatures, structures, functors, values} =
0863bb353065 more systematic type use_context;
wenzelm
parents: 30677
diff changeset
   100
      let
0863bb353065 more systematic type use_context;
wenzelm
parents: 30677
diff changeset
   101
        fun add_prefix prefix (PrettyBlock (ind, consistent, context, prts)) =
0863bb353065 more systematic type use_context;
wenzelm
parents: 30677
diff changeset
   102
              let
0863bb353065 more systematic type use_context;
wenzelm
parents: 30677
diff changeset
   103
                fun make_prefix context =
0863bb353065 more systematic type use_context;
wenzelm
parents: 30677
diff changeset
   104
                  (case get_first (fn ContextParentStructure p => SOME p | _ => NONE) context of
0863bb353065 more systematic type use_context;
wenzelm
parents: 30677
diff changeset
   105
                    SOME (name, sub_context) => make_prefix sub_context ^ name ^ "."
0863bb353065 more systematic type use_context;
wenzelm
parents: 30677
diff changeset
   106
                  | NONE => prefix);
0863bb353065 more systematic type use_context;
wenzelm
parents: 30677
diff changeset
   107
                val this_prefix = make_prefix context;
0863bb353065 more systematic type use_context;
wenzelm
parents: 30677
diff changeset
   108
              in PrettyBlock (ind, consistent, context, map (add_prefix this_prefix) prts) end
0863bb353065 more systematic type use_context;
wenzelm
parents: 30677
diff changeset
   109
          | add_prefix prefix (prt as PrettyString s) =
0863bb353065 more systematic type use_context;
wenzelm
parents: 30677
diff changeset
   110
              if prefix = "" then prt else PrettyString (prefix ^ s)
0863bb353065 more systematic type use_context;
wenzelm
parents: 30677
diff changeset
   111
          | add_prefix _ (prt as PrettyBreak _) = prt;
0863bb353065 more systematic type use_context;
wenzelm
parents: 30677
diff changeset
   112
0863bb353065 more systematic type use_context;
wenzelm
parents: 30677
diff changeset
   113
        val depth = get_print_depth ();
0863bb353065 more systematic type use_context;
wenzelm
parents: 30677
diff changeset
   114
        val with_struct = ! PolyML.Compiler.printTypesWithStructureName;
0863bb353065 more systematic type use_context;
wenzelm
parents: 30677
diff changeset
   115
0863bb353065 more systematic type use_context;
wenzelm
parents: 30677
diff changeset
   116
        fun display disp x =
0863bb353065 more systematic type use_context;
wenzelm
parents: 30677
diff changeset
   117
          if depth > 0 then
0863bb353065 more systematic type use_context;
wenzelm
parents: 30677
diff changeset
   118
            (disp x
0863bb353065 more systematic type use_context;
wenzelm
parents: 30677
diff changeset
   119
              |> with_struct ? add_prefix ""
0863bb353065 more systematic type use_context;
wenzelm
parents: 30677
diff changeset
   120
              |> pretty_ml |> Pretty.from_ML |> Pretty.string_of |> put; put "\n")
0863bb353065 more systematic type use_context;
wenzelm
parents: 30677
diff changeset
   121
          else ();
0863bb353065 more systematic type use_context;
wenzelm
parents: 30677
diff changeset
   122
0863bb353065 more systematic type use_context;
wenzelm
parents: 30677
diff changeset
   123
        fun apply_fix (a, b) =
0863bb353065 more systematic type use_context;
wenzelm
parents: 30677
diff changeset
   124
          (display PolyML.NameSpace.displayFix (a, b); #enterFix space (a, b));
0863bb353065 more systematic type use_context;
wenzelm
parents: 30677
diff changeset
   125
        fun apply_type (a, b) =
0863bb353065 more systematic type use_context;
wenzelm
parents: 30677
diff changeset
   126
          (display PolyML.NameSpace.displayType (b, depth); #enterType space (a, b));
0863bb353065 more systematic type use_context;
wenzelm
parents: 30677
diff changeset
   127
        fun apply_sig (a, b) =
0863bb353065 more systematic type use_context;
wenzelm
parents: 30677
diff changeset
   128
          (display PolyML.NameSpace.displaySig (b, depth, space); #enterSig space (a, b));
0863bb353065 more systematic type use_context;
wenzelm
parents: 30677
diff changeset
   129
        fun apply_struct (a, b) =
0863bb353065 more systematic type use_context;
wenzelm
parents: 30677
diff changeset
   130
          (display PolyML.NameSpace.displayStruct (b, depth, space); #enterStruct space (a, b));
0863bb353065 more systematic type use_context;
wenzelm
parents: 30677
diff changeset
   131
        fun apply_funct (a, b) =
0863bb353065 more systematic type use_context;
wenzelm
parents: 30677
diff changeset
   132
          (display PolyML.NameSpace.displayFunct (b, depth, space); #enterFunct space (a, b));
0863bb353065 more systematic type use_context;
wenzelm
parents: 30677
diff changeset
   133
        fun apply_val (a, b) =
0863bb353065 more systematic type use_context;
wenzelm
parents: 30677
diff changeset
   134
          (display PolyML.NameSpace.displayVal (b, depth, space); #enterVal space (a, b));
0863bb353065 more systematic type use_context;
wenzelm
parents: 30677
diff changeset
   135
      in
0863bb353065 more systematic type use_context;
wenzelm
parents: 30677
diff changeset
   136
        List.app apply_fix fixes;
0863bb353065 more systematic type use_context;
wenzelm
parents: 30677
diff changeset
   137
        List.app apply_type types;
0863bb353065 more systematic type use_context;
wenzelm
parents: 30677
diff changeset
   138
        List.app apply_sig signatures;
0863bb353065 more systematic type use_context;
wenzelm
parents: 30677
diff changeset
   139
        List.app apply_struct structures;
0863bb353065 more systematic type use_context;
wenzelm
parents: 30677
diff changeset
   140
        List.app apply_funct functors;
0863bb353065 more systematic type use_context;
wenzelm
parents: 30677
diff changeset
   141
        List.app apply_val values
0863bb353065 more systematic type use_context;
wenzelm
parents: 30677
diff changeset
   142
      end;
0863bb353065 more systematic type use_context;
wenzelm
parents: 30677
diff changeset
   143
30704
d6d4828e74a2 register token positions persistently with context;
wenzelm
parents: 30681
diff changeset
   144
    fun result_fun (phase1, phase2) () =
d6d4828e74a2 register token positions persistently with context;
wenzelm
parents: 30681
diff changeset
   145
     (case phase1 of NONE => ()
d6d4828e74a2 register token positions persistently with context;
wenzelm
parents: 30681
diff changeset
   146
      | SOME parse_tree => report_parse_tree (the (Context.thread_data ())) parse_tree;
d6d4828e74a2 register token positions persistently with context;
wenzelm
parents: 30681
diff changeset
   147
      case phase2 of NONE => error "Static Errors"
d6d4828e74a2 register token positions persistently with context;
wenzelm
parents: 30681
diff changeset
   148
      | SOME code => apply_result (Toplevel.program code));
30680
0863bb353065 more systematic type use_context;
wenzelm
parents: 30677
diff changeset
   149
0863bb353065 more systematic type use_context;
wenzelm
parents: 30677
diff changeset
   150
0863bb353065 more systematic type use_context;
wenzelm
parents: 30677
diff changeset
   151
    (* compiler invocation *)
30646
d26ad4576d5c proper signature;
wenzelm
parents: 30644
diff changeset
   152
30640
3f3d1e218b64 Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff changeset
   153
    val parameters =
3f3d1e218b64 Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff changeset
   154
     [PolyML.Compiler.CPOutStream put,
30680
0863bb353065 more systematic type use_context;
wenzelm
parents: 30677
diff changeset
   155
      PolyML.Compiler.CPNameSpace space,
30640
3f3d1e218b64 Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff changeset
   156
      PolyML.Compiler.CPErrorMessageProc put_message,
3f3d1e218b64 Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff changeset
   157
      PolyML.Compiler.CPLineNo (fn () => ! current_line),
30704
d6d4828e74a2 register token positions persistently with context;
wenzelm
parents: 30681
diff changeset
   158
      PolyML.Compiler.CPFileName (the_default "ML" (Position.file_of pos)),
30640
3f3d1e218b64 Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff changeset
   159
      PolyML.Compiler.CPLineOffset get_index,
30680
0863bb353065 more systematic type use_context;
wenzelm
parents: 30677
diff changeset
   160
      PolyML.Compiler.CPCompilerResultFun result_fun];
30640
3f3d1e218b64 Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff changeset
   161
    val _ =
30704
d6d4828e74a2 register token positions persistently with context;
wenzelm
parents: 30681
diff changeset
   162
      (while not (List.null (! input_buffer)) do
30640
3f3d1e218b64 Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff changeset
   163
        PolyML.compiler (get, parameters) ())
3f3d1e218b64 Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff changeset
   164
      handle exn =>
3f3d1e218b64 Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff changeset
   165
       (put ("Exception- " ^ General.exnMessage exn ^ " raised");
30677
df6ca2f50199 eliminated Output.ml_output;
wenzelm
parents: 30668
diff changeset
   166
        error (output ()); raise exn);
30680
0863bb353065 more systematic type use_context;
wenzelm
parents: 30677
diff changeset
   167
  in if verbose then print (output ()) else () end;
0863bb353065 more systematic type use_context;
wenzelm
parents: 30677
diff changeset
   168
0863bb353065 more systematic type use_context;
wenzelm
parents: 30677
diff changeset
   169
val eval = use_text ML_Context.local_context;
30640
3f3d1e218b64 Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff changeset
   170
3f3d1e218b64 Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff changeset
   171
3f3d1e218b64 Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff changeset
   172
(* ML test command *)
3f3d1e218b64 Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff changeset
   173
30680
0863bb353065 more systematic type use_context;
wenzelm
parents: 30677
diff changeset
   174
fun ML_test (txt, pos) =
30640
3f3d1e218b64 Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff changeset
   175
  let
3f3d1e218b64 Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff changeset
   176
    val _ = Position.report Markup.ML_source pos;
30644
2948f4494e86 ML_Lex.read_antiq;
wenzelm
parents: 30640
diff changeset
   177
    val ants = ML_Lex.read_antiq (Symbol_Pos.explode (txt, pos), pos);
30640
3f3d1e218b64 Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff changeset
   178
    val ((env, body), env_ctxt) = ML_Context.eval_antiquotes (ants, pos) (Context.thread_data ());
3f3d1e218b64 Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff changeset
   179
3f3d1e218b64 Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff changeset
   180
    val _ = Context.setmp_thread_data env_ctxt
30680
0863bb353065 more systematic type use_context;
wenzelm
parents: 30677
diff changeset
   181
        (fn () => (eval false Position.none env; Context.thread_data ())) ()
30704
d6d4828e74a2 register token positions persistently with context;
wenzelm
parents: 30681
diff changeset
   182
      |> (fn NONE => () | SOME context' => Context.>> (inherit_env context'));
30680
0863bb353065 more systematic type use_context;
wenzelm
parents: 30677
diff changeset
   183
    val _ = eval true pos body;
0863bb353065 more systematic type use_context;
wenzelm
parents: 30677
diff changeset
   184
    val _ = eval false Position.none (ML_Lex.tokenize "structure Isabelle = struct end");
30640
3f3d1e218b64 Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff changeset
   185
  in () end;
3f3d1e218b64 Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff changeset
   186
30644
2948f4494e86 ML_Lex.read_antiq;
wenzelm
parents: 30640
diff changeset
   187
30640
3f3d1e218b64 Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff changeset
   188
local structure P = OuterParse and K = OuterKeyword in
3f3d1e218b64 Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff changeset
   189
30704
d6d4828e74a2 register token positions persistently with context;
wenzelm
parents: 30681
diff changeset
   190
fun propagate_env (context as Context.Proof lthy) =
d6d4828e74a2 register token positions persistently with context;
wenzelm
parents: 30681
diff changeset
   191
      Context.Proof (LocalTheory.map_contexts (inherit_env context) lthy)
d6d4828e74a2 register token positions persistently with context;
wenzelm
parents: 30681
diff changeset
   192
  | propagate_env context = context;
30644
2948f4494e86 ML_Lex.read_antiq;
wenzelm
parents: 30640
diff changeset
   193
30640
3f3d1e218b64 Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff changeset
   194
val _ =
30644
2948f4494e86 ML_Lex.read_antiq;
wenzelm
parents: 30640
diff changeset
   195
  OuterSyntax.command "ML_test" "advanced ML compiler test" (K.tag_ml K.thy_decl)
2948f4494e86 ML_Lex.read_antiq;
wenzelm
parents: 30640
diff changeset
   196
    (P.ML_source >> (fn src =>
30704
d6d4828e74a2 register token positions persistently with context;
wenzelm
parents: 30681
diff changeset
   197
      Toplevel.generic_theory (ML_Context.exec (fn () => ML_test src) #> propagate_env)));
30640
3f3d1e218b64 Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff changeset
   198
3f3d1e218b64 Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff changeset
   199
end;
3f3d1e218b64 Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff changeset
   200
3f3d1e218b64 Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff changeset
   201
end;
3f3d1e218b64 Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff changeset
   202