src/Pure/ML-Systems/polyml_common.ML
changeset 31686 e54ae15335a1
parent 31324 3ffa005c7701
child 32737 76fa673eee8b
equal deleted inserted replaced
31685:c124445a4b61 31686:e54ae15335a1
     6 exception Interrupt = SML90.Interrupt;
     6 exception Interrupt = SML90.Interrupt;
     7 
     7 
     8 use "ML-Systems/exn.ML";
     8 use "ML-Systems/exn.ML";
     9 use "ML-Systems/multithreading.ML";
     9 use "ML-Systems/multithreading.ML";
    10 use "ML-Systems/time_limit.ML";
    10 use "ML-Systems/time_limit.ML";
       
    11 use "ML-Systems/timing.ML";
    11 use "ML-Systems/system_shell.ML";
    12 use "ML-Systems/system_shell.ML";
    12 use "ML-Systems/ml_pretty.ML";
    13 use "ML-Systems/ml_pretty.ML";
    13 use "ML-Systems/use_context.ML";
    14 use "ML-Systems/use_context.ML";
    14 
    15 
    15 
    16 
    37 
    38 
    38 val ord = SML90.ord;
    39 val ord = SML90.ord;
    39 val chr = SML90.chr;
    40 val chr = SML90.chr;
    40 val explode = SML90.explode;
    41 val explode = SML90.explode;
    41 val implode = SML90.implode;
    42 val implode = SML90.implode;
    42 
       
    43 
       
    44 (* compiler-independent timing functions *)
       
    45 
       
    46 fun start_timing () =
       
    47   let
       
    48     val timer = Timer.startCPUTimer ();
       
    49     val time = Timer.checkCPUTimer timer;
       
    50   in (timer, time) end;
       
    51 
       
    52 fun end_timing (timer, {sys, usr}) =
       
    53   let
       
    54     open Time;  (*...for Time.toString, Time.+ and Time.- *)
       
    55     val {sys = sys2, usr = usr2} = Timer.checkCPUTimer timer;
       
    56     val user = usr2 - usr;
       
    57     val all = user + sys2 - sys;
       
    58     val message = "User " ^ toString user ^ "  All "^ toString all ^ " secs" handle Time => "";
       
    59   in {message = message, user = user, all = all} end;
       
    60 
       
    61 fun check_timer timer =
       
    62   let
       
    63     val {sys, usr} = Timer.checkCPUTimer timer;
       
    64     val gc = Timer.checkGCTime timer;    (* FIXME already included in usr? *)
       
    65   in (sys, usr, gc) end;
       
    66 
    43 
    67 
    44 
    68 (* prompts *)
    45 (* prompts *)
    69 
    46 
    70 fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2);
    47 fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2);