Admin/polyml/future/ROOT.ML
changeset 44151 e842a2cf923c
parent 44150 d0d76f40d7a0
child 44154 4231c55b2d5e
equal deleted inserted replaced
44150:d0d76f40d7a0 44151:e842a2cf923c
     8 
     8 
     9 use "General/basics.ML";
     9 use "General/basics.ML";
    10 use "library.ML";
    10 use "library.ML";
    11 use "General/alist.ML";
    11 use "General/alist.ML";
    12 use "General/table.ML";
    12 use "General/table.ML";
    13 use "General/queue.ML";
       
    14 use "General/graph.ML";
    13 use "General/graph.ML";
       
    14 
       
    15 structure Position =
       
    16 struct
       
    17   fun thread_data () = ();
       
    18   fun setmp_thread_data () f x = f x;
       
    19 end;
       
    20 
       
    21 structure Output =
       
    22 struct
       
    23   type output = string;
       
    24   fun escape s : output = s;
       
    25   fun raw_stdout s = (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut);
       
    26   fun writeln s = raw_stdout (suffix "\n" s);
       
    27   fun warning s = writeln (prefix_lines "### " s);
       
    28   fun status (_: string) = ();
       
    29 end;
       
    30 val writeln = Output.writeln;
       
    31 val warning = Output.warning;
       
    32 fun print_mode_value () : string list = [];
       
    33 
       
    34 use "General/properties.ML";
       
    35 use "General/timing.ML";
    15 
    36 
    16 use "Concurrent/simple_thread.ML";
    37 use "Concurrent/simple_thread.ML";
    17 use "Concurrent/synchronized.ML";
    38 use "Concurrent/synchronized.ML";
    18 
       
    19 use "General/properties.ML";
       
    20 use "General/print_mode.ML";
       
    21 use "General/output.ML";
       
    22 use "General/timing.ML";
       
    23 use "General/markup.ML";
    39 use "General/markup.ML";
    24 use "General/scan.ML";
       
    25 use "General/source.ML";
       
    26 use "General/symbol.ML";
       
    27 use "General/position.ML";
       
    28 
       
    29 use "Concurrent/single_assignment.ML";
    40 use "Concurrent/single_assignment.ML";
    30 use "Concurrent/time_limit.ML";
    41 use "Concurrent/time_limit.ML";
    31 use "Concurrent/mailbox.ML";
       
    32 use "Concurrent/task_queue.ML";
    42 use "Concurrent/task_queue.ML";
    33 use "Concurrent/future.ML";
    43 use "Concurrent/future.ML";
    34 use "Concurrent/lazy.ML";
    44 use "Concurrent/lazy.ML";
    35 use "Concurrent/par_list.ML";
    45 use "Concurrent/par_list.ML";
       
    46 
       
    47 use "General/queue.ML";
       
    48 use "Concurrent/mailbox.ML";
    36 use "Concurrent/cache.ML";
    49 use "Concurrent/cache.ML";
    37 
    50 
    38 PolyML.addPrettyPrinter (fn depth => fn pretty => fn var =>
    51 PolyML.addPrettyPrinter (fn depth => fn pretty => fn var =>
    39   pretty (Synchronized.value var, depth));
    52   pretty (Synchronized.value var, depth));
    40 
    53