Admin/polyml/future/ROOT.ML
author blanchet
Mon, 19 May 2014 23:43:53 +0200
changeset 57005 33f3d2ea803d
parent 44334 605381e7c7c5
child 61556 0d4ee4168e41
permissions -rw-r--r--
store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
44148
a34e6e292115 prefix of Pure/ROOT.ML required for concurrency within the ML runtime;
wenzelm
parents:
diff changeset
     1
a34e6e292115 prefix of Pure/ROOT.ML required for concurrency within the ML runtime;
wenzelm
parents:
diff changeset
     2
fun exit 0 = (OS.Process.exit OS.Process.success): unit
a34e6e292115 prefix of Pure/ROOT.ML required for concurrency within the ML runtime;
wenzelm
parents:
diff changeset
     3
  | exit _ = OS.Process.exit OS.Process.failure;
a34e6e292115 prefix of Pure/ROOT.ML required for concurrency within the ML runtime;
wenzelm
parents:
diff changeset
     4
44154
4231c55b2d5e disentangled nested ML files;
wenzelm
parents: 44151
diff changeset
     5
fun reraise exn =
4231c55b2d5e disentangled nested ML files;
wenzelm
parents: 44151
diff changeset
     6
  (case PolyML.exceptionLocation exn of
4231c55b2d5e disentangled nested ML files;
wenzelm
parents: 44151
diff changeset
     7
    NONE => raise exn
4231c55b2d5e disentangled nested ML files;
wenzelm
parents: 44151
diff changeset
     8
  | SOME location => PolyML.raiseWithLocation (exn, location));
4231c55b2d5e disentangled nested ML files;
wenzelm
parents: 44151
diff changeset
     9
44258
a93426812ad5 follow updates of Isabelle/Pure;
wenzelm
parents: 44154
diff changeset
    10
fun set_exn_serial i exn =
a93426812ad5 follow updates of Isabelle/Pure;
wenzelm
parents: 44154
diff changeset
    11
  let
a93426812ad5 follow updates of Isabelle/Pure;
wenzelm
parents: 44154
diff changeset
    12
    val (file, startLine, endLine) =
a93426812ad5 follow updates of Isabelle/Pure;
wenzelm
parents: 44154
diff changeset
    13
      (case PolyML.exceptionLocation exn of
a93426812ad5 follow updates of Isabelle/Pure;
wenzelm
parents: 44154
diff changeset
    14
        NONE => ("", 0, 0)
a93426812ad5 follow updates of Isabelle/Pure;
wenzelm
parents: 44154
diff changeset
    15
      | SOME {file, startLine, endLine, startPosition, ...} => (file, startLine, endLine));
a93426812ad5 follow updates of Isabelle/Pure;
wenzelm
parents: 44154
diff changeset
    16
    val location =
a93426812ad5 follow updates of Isabelle/Pure;
wenzelm
parents: 44154
diff changeset
    17
      {file = file, startLine = startLine, endLine = endLine,
a93426812ad5 follow updates of Isabelle/Pure;
wenzelm
parents: 44154
diff changeset
    18
        startPosition = ~ i, endPosition = 0};
a93426812ad5 follow updates of Isabelle/Pure;
wenzelm
parents: 44154
diff changeset
    19
  in PolyML.raiseWithLocation (exn, location) handle e => e end;
a93426812ad5 follow updates of Isabelle/Pure;
wenzelm
parents: 44154
diff changeset
    20
a93426812ad5 follow updates of Isabelle/Pure;
wenzelm
parents: 44154
diff changeset
    21
fun get_exn_serial exn =
a93426812ad5 follow updates of Isabelle/Pure;
wenzelm
parents: 44154
diff changeset
    22
  (case Option.map #startPosition (PolyML.exceptionLocation exn) of
a93426812ad5 follow updates of Isabelle/Pure;
wenzelm
parents: 44154
diff changeset
    23
    NONE => NONE
a93426812ad5 follow updates of Isabelle/Pure;
wenzelm
parents: 44154
diff changeset
    24
  | SOME i => if i >= 0 then NONE else SOME (~ i));
a93426812ad5 follow updates of Isabelle/Pure;
wenzelm
parents: 44154
diff changeset
    25
44154
4231c55b2d5e disentangled nested ML files;
wenzelm
parents: 44151
diff changeset
    26
exception Interrupt = SML90.Interrupt;
4231c55b2d5e disentangled nested ML files;
wenzelm
parents: 44151
diff changeset
    27
val ord = SML90.ord;
4231c55b2d5e disentangled nested ML files;
wenzelm
parents: 44151
diff changeset
    28
val chr = SML90.chr;
4231c55b2d5e disentangled nested ML files;
wenzelm
parents: 44151
diff changeset
    29
val raw_explode = SML90.explode;
4231c55b2d5e disentangled nested ML files;
wenzelm
parents: 44151
diff changeset
    30
val implode = SML90.implode;
4231c55b2d5e disentangled nested ML files;
wenzelm
parents: 44151
diff changeset
    31
4231c55b2d5e disentangled nested ML files;
wenzelm
parents: 44151
diff changeset
    32
val pointer_eq = PolyML.pointerEq;
4231c55b2d5e disentangled nested ML files;
wenzelm
parents: 44151
diff changeset
    33
4231c55b2d5e disentangled nested ML files;
wenzelm
parents: 44151
diff changeset
    34
val exception_trace = PolyML.exception_trace;
4231c55b2d5e disentangled nested ML files;
wenzelm
parents: 44151
diff changeset
    35
4231c55b2d5e disentangled nested ML files;
wenzelm
parents: 44151
diff changeset
    36
open Thread;
4231c55b2d5e disentangled nested ML files;
wenzelm
parents: 44151
diff changeset
    37
val seconds = Time.fromReal;
4231c55b2d5e disentangled nested ML files;
wenzelm
parents: 44151
diff changeset
    38
use "General/exn.ML";
4231c55b2d5e disentangled nested ML files;
wenzelm
parents: 44151
diff changeset
    39
use "ML-Systems/multithreading.ML";
4231c55b2d5e disentangled nested ML files;
wenzelm
parents: 44151
diff changeset
    40
use "ML-Systems/multithreading_polyml.ML";
4231c55b2d5e disentangled nested ML files;
wenzelm
parents: 44151
diff changeset
    41
use "ML-Systems/unsynchronized.ML";
4231c55b2d5e disentangled nested ML files;
wenzelm
parents: 44151
diff changeset
    42
4231c55b2d5e disentangled nested ML files;
wenzelm
parents: 44151
diff changeset
    43
use "ML-Systems/ml_pretty.ML";
44148
a34e6e292115 prefix of Pure/ROOT.ML required for concurrency within the ML runtime;
wenzelm
parents:
diff changeset
    44
44154
4231c55b2d5e disentangled nested ML files;
wenzelm
parents: 44151
diff changeset
    45
val pretty_ml =
4231c55b2d5e disentangled nested ML files;
wenzelm
parents: 44151
diff changeset
    46
  let
4231c55b2d5e disentangled nested ML files;
wenzelm
parents: 44151
diff changeset
    47
    fun convert len (PolyML.PrettyBlock (ind, _, context, prts)) =
4231c55b2d5e disentangled nested ML files;
wenzelm
parents: 44151
diff changeset
    48
          let
4231c55b2d5e disentangled nested ML files;
wenzelm
parents: 44151
diff changeset
    49
            fun property name default =
4231c55b2d5e disentangled nested ML files;
wenzelm
parents: 44151
diff changeset
    50
              (case List.find (fn PolyML.ContextProperty (a, _) => name = a | _ => false) context of
4231c55b2d5e disentangled nested ML files;
wenzelm
parents: 44151
diff changeset
    51
                SOME (PolyML.ContextProperty (_, b)) => b
4231c55b2d5e disentangled nested ML files;
wenzelm
parents: 44151
diff changeset
    52
              | NONE => default);
4231c55b2d5e disentangled nested ML files;
wenzelm
parents: 44151
diff changeset
    53
            val bg = property "begin" "";
4231c55b2d5e disentangled nested ML files;
wenzelm
parents: 44151
diff changeset
    54
            val en = property "end" "";
4231c55b2d5e disentangled nested ML files;
wenzelm
parents: 44151
diff changeset
    55
            val len' = property "length" len;
4231c55b2d5e disentangled nested ML files;
wenzelm
parents: 44151
diff changeset
    56
          in ML_Pretty.Block ((bg, en), map (convert len') prts, ind) end
4231c55b2d5e disentangled nested ML files;
wenzelm
parents: 44151
diff changeset
    57
      | convert len (PolyML.PrettyString s) =
4231c55b2d5e disentangled nested ML files;
wenzelm
parents: 44151
diff changeset
    58
          ML_Pretty.String (s, case Int.fromString len of SOME i => i | NONE => size s)
4231c55b2d5e disentangled nested ML files;
wenzelm
parents: 44151
diff changeset
    59
      | convert _ (PolyML.PrettyBreak (wd, _)) =
4231c55b2d5e disentangled nested ML files;
wenzelm
parents: 44151
diff changeset
    60
          ML_Pretty.Break (if wd < 99999 then (false, wd) else (true, 2));
4231c55b2d5e disentangled nested ML files;
wenzelm
parents: 44151
diff changeset
    61
  in convert "" end;
4231c55b2d5e disentangled nested ML files;
wenzelm
parents: 44151
diff changeset
    62
4231c55b2d5e disentangled nested ML files;
wenzelm
parents: 44151
diff changeset
    63
fun ml_pretty (ML_Pretty.Block ((bg, en), prts, ind)) =
4231c55b2d5e disentangled nested ML files;
wenzelm
parents: 44151
diff changeset
    64
      let val context =
4231c55b2d5e disentangled nested ML files;
wenzelm
parents: 44151
diff changeset
    65
        (if bg = "" then [] else [PolyML.ContextProperty ("begin", bg)]) @
4231c55b2d5e disentangled nested ML files;
wenzelm
parents: 44151
diff changeset
    66
        (if en = "" then [] else [PolyML.ContextProperty ("end", en)])
4231c55b2d5e disentangled nested ML files;
wenzelm
parents: 44151
diff changeset
    67
      in PolyML.PrettyBlock (ind, false, context, map ml_pretty prts) end
4231c55b2d5e disentangled nested ML files;
wenzelm
parents: 44151
diff changeset
    68
  | ml_pretty (ML_Pretty.String (s, len)) =
4231c55b2d5e disentangled nested ML files;
wenzelm
parents: 44151
diff changeset
    69
      if len = size s then PolyML.PrettyString s
4231c55b2d5e disentangled nested ML files;
wenzelm
parents: 44151
diff changeset
    70
      else PolyML.PrettyBlock
4231c55b2d5e disentangled nested ML files;
wenzelm
parents: 44151
diff changeset
    71
        (0, false, [PolyML.ContextProperty ("length", Int.toString len)], [PolyML.PrettyString s])
4231c55b2d5e disentangled nested ML files;
wenzelm
parents: 44151
diff changeset
    72
  | ml_pretty (ML_Pretty.Break (false, wd)) = PolyML.PrettyBreak (wd, 0)
4231c55b2d5e disentangled nested ML files;
wenzelm
parents: 44151
diff changeset
    73
  | ml_pretty (ML_Pretty.Break (true, _)) = PolyML.PrettyBreak (99999, 0);
44148
a34e6e292115 prefix of Pure/ROOT.ML required for concurrency within the ML runtime;
wenzelm
parents:
diff changeset
    74
a34e6e292115 prefix of Pure/ROOT.ML required for concurrency within the ML runtime;
wenzelm
parents:
diff changeset
    75
use "General/basics.ML";
a34e6e292115 prefix of Pure/ROOT.ML required for concurrency within the ML runtime;
wenzelm
parents:
diff changeset
    76
use "library.ML";
a34e6e292115 prefix of Pure/ROOT.ML required for concurrency within the ML runtime;
wenzelm
parents:
diff changeset
    77
use "General/alist.ML";
a34e6e292115 prefix of Pure/ROOT.ML required for concurrency within the ML runtime;
wenzelm
parents:
diff changeset
    78
use "General/table.ML";
44149
fdf0af3eaeb9 some trimming;
wenzelm
parents: 44148
diff changeset
    79
use "General/graph.ML";
44258
a93426812ad5 follow updates of Isabelle/Pure;
wenzelm
parents: 44154
diff changeset
    80
use "General/ord_list.ML";
44148
a34e6e292115 prefix of Pure/ROOT.ML required for concurrency within the ML runtime;
wenzelm
parents:
diff changeset
    81
44151
e842a2cf923c more trimming;
wenzelm
parents: 44150
diff changeset
    82
structure Position =
e842a2cf923c more trimming;
wenzelm
parents: 44150
diff changeset
    83
struct
e842a2cf923c more trimming;
wenzelm
parents: 44150
diff changeset
    84
  fun thread_data () = ();
e842a2cf923c more trimming;
wenzelm
parents: 44150
diff changeset
    85
  fun setmp_thread_data () f x = f x;
e842a2cf923c more trimming;
wenzelm
parents: 44150
diff changeset
    86
end;
e842a2cf923c more trimming;
wenzelm
parents: 44150
diff changeset
    87
e842a2cf923c more trimming;
wenzelm
parents: 44150
diff changeset
    88
structure Output =
e842a2cf923c more trimming;
wenzelm
parents: 44150
diff changeset
    89
struct
e842a2cf923c more trimming;
wenzelm
parents: 44150
diff changeset
    90
  type output = string;
e842a2cf923c more trimming;
wenzelm
parents: 44150
diff changeset
    91
  fun escape s : output = s;
e842a2cf923c more trimming;
wenzelm
parents: 44150
diff changeset
    92
  fun raw_stdout s = (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut);
e842a2cf923c more trimming;
wenzelm
parents: 44150
diff changeset
    93
  fun writeln s = raw_stdout (suffix "\n" s);
e842a2cf923c more trimming;
wenzelm
parents: 44150
diff changeset
    94
  fun warning s = writeln (prefix_lines "### " s);
e842a2cf923c more trimming;
wenzelm
parents: 44150
diff changeset
    95
  fun status (_: string) = ();
e842a2cf923c more trimming;
wenzelm
parents: 44150
diff changeset
    96
end;
e842a2cf923c more trimming;
wenzelm
parents: 44150
diff changeset
    97
val writeln = Output.writeln;
e842a2cf923c more trimming;
wenzelm
parents: 44150
diff changeset
    98
val warning = Output.warning;
e842a2cf923c more trimming;
wenzelm
parents: 44150
diff changeset
    99
fun print_mode_value () : string list = [];
e842a2cf923c more trimming;
wenzelm
parents: 44150
diff changeset
   100
e842a2cf923c more trimming;
wenzelm
parents: 44150
diff changeset
   101
use "General/properties.ML";
e842a2cf923c more trimming;
wenzelm
parents: 44150
diff changeset
   102
use "General/timing.ML";
e842a2cf923c more trimming;
wenzelm
parents: 44150
diff changeset
   103
44148
a34e6e292115 prefix of Pure/ROOT.ML required for concurrency within the ML runtime;
wenzelm
parents:
diff changeset
   104
use "Concurrent/simple_thread.ML";
a34e6e292115 prefix of Pure/ROOT.ML required for concurrency within the ML runtime;
wenzelm
parents:
diff changeset
   105
use "Concurrent/synchronized.ML";
a34e6e292115 prefix of Pure/ROOT.ML required for concurrency within the ML runtime;
wenzelm
parents:
diff changeset
   106
use "General/markup.ML";
a34e6e292115 prefix of Pure/ROOT.ML required for concurrency within the ML runtime;
wenzelm
parents:
diff changeset
   107
use "Concurrent/single_assignment.ML";
44149
fdf0af3eaeb9 some trimming;
wenzelm
parents: 44148
diff changeset
   108
use "Concurrent/time_limit.ML";
44258
a93426812ad5 follow updates of Isabelle/Pure;
wenzelm
parents: 44154
diff changeset
   109
use "Concurrent/par_exn.ML";
44148
a34e6e292115 prefix of Pure/ROOT.ML required for concurrency within the ML runtime;
wenzelm
parents:
diff changeset
   110
use "Concurrent/task_queue.ML";
a34e6e292115 prefix of Pure/ROOT.ML required for concurrency within the ML runtime;
wenzelm
parents:
diff changeset
   111
use "Concurrent/future.ML";
a34e6e292115 prefix of Pure/ROOT.ML required for concurrency within the ML runtime;
wenzelm
parents:
diff changeset
   112
use "Concurrent/lazy.ML";
a34e6e292115 prefix of Pure/ROOT.ML required for concurrency within the ML runtime;
wenzelm
parents:
diff changeset
   113
use "Concurrent/par_list.ML";
44151
e842a2cf923c more trimming;
wenzelm
parents: 44150
diff changeset
   114
e842a2cf923c more trimming;
wenzelm
parents: 44150
diff changeset
   115
use "General/queue.ML";
e842a2cf923c more trimming;
wenzelm
parents: 44150
diff changeset
   116
use "Concurrent/mailbox.ML";
44148
a34e6e292115 prefix of Pure/ROOT.ML required for concurrency within the ML runtime;
wenzelm
parents:
diff changeset
   117
use "Concurrent/cache.ML";
a34e6e292115 prefix of Pure/ROOT.ML required for concurrency within the ML runtime;
wenzelm
parents:
diff changeset
   118
44150
d0d76f40d7a0 recovered some ML toplevel pp;
wenzelm
parents: 44149
diff changeset
   119
PolyML.addPrettyPrinter (fn depth => fn pretty => fn var =>
d0d76f40d7a0 recovered some ML toplevel pp;
wenzelm
parents: 44149
diff changeset
   120
  pretty (Synchronized.value var, depth));
d0d76f40d7a0 recovered some ML toplevel pp;
wenzelm
parents: 44149
diff changeset
   121
d0d76f40d7a0 recovered some ML toplevel pp;
wenzelm
parents: 44149
diff changeset
   122
PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
d0d76f40d7a0 recovered some ML toplevel pp;
wenzelm
parents: 44149
diff changeset
   123
  (case Future.peek x of
d0d76f40d7a0 recovered some ML toplevel pp;
wenzelm
parents: 44149
diff changeset
   124
    NONE => PolyML.PrettyString "<future>"
d0d76f40d7a0 recovered some ML toplevel pp;
wenzelm
parents: 44149
diff changeset
   125
  | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
d0d76f40d7a0 recovered some ML toplevel pp;
wenzelm
parents: 44149
diff changeset
   126
  | SOME (Exn.Res y) => pretty (y, depth)));
d0d76f40d7a0 recovered some ML toplevel pp;
wenzelm
parents: 44149
diff changeset
   127
d0d76f40d7a0 recovered some ML toplevel pp;
wenzelm
parents: 44149
diff changeset
   128
PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
d0d76f40d7a0 recovered some ML toplevel pp;
wenzelm
parents: 44149
diff changeset
   129
  (case Lazy.peek x of
d0d76f40d7a0 recovered some ML toplevel pp;
wenzelm
parents: 44149
diff changeset
   130
    NONE => PolyML.PrettyString "<lazy>"
d0d76f40d7a0 recovered some ML toplevel pp;
wenzelm
parents: 44149
diff changeset
   131
  | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
d0d76f40d7a0 recovered some ML toplevel pp;
wenzelm
parents: 44149
diff changeset
   132
  | SOME (Exn.Res y) => pretty (y, depth)));
d0d76f40d7a0 recovered some ML toplevel pp;
wenzelm
parents: 44149
diff changeset
   133