src/Pure/ROOT.ML
changeset 62508 d0b68218ea55
parent 62501 98fa1f9a292f
child 62516 5732f1c31566
     1.1 --- a/src/Pure/ROOT.ML	Thu Mar 03 21:35:16 2016 +0100
     1.2 +++ b/src/Pure/ROOT.ML	Thu Mar 03 21:59:21 2016 +0100
     1.3 @@ -1,6 +1,14 @@
     1.4 -(*** Isabelle/Pure bootstrap from "RAW" environment ***)
     1.5 +(*** Isabelle/Pure bootstrap from RAW_ML_SYSTEM ***)
     1.6 +
     1.7 +(** bootstrap phase 0: Poly/ML setup **)
     1.8 +
     1.9 +(* initial ML name space *)
    1.10  
    1.11 -(** bootstrap phase 0: towards ML within position context *)
    1.12 +use "ML/ml_system.ML";
    1.13 +use "ML/ml_name_space.ML";
    1.14 +
    1.15 +if List.exists (fn (a, _) => a = "FixedInt") (#allStruct ML_Name_Space.global ()) then ()
    1.16 +else use "ML/fixed_int_dummy.ML";
    1.17  
    1.18  structure Distribution =     (*filled-in by makedist*)
    1.19  struct
    1.20 @@ -10,6 +18,87 @@
    1.21  end;
    1.22  
    1.23  
    1.24 +(* multithreading *)
    1.25 +
    1.26 +use "General/exn.ML";
    1.27 +
    1.28 +val seconds = Time.fromReal;
    1.29 +
    1.30 +open Thread;
    1.31 +use "Concurrent/multithreading.ML";
    1.32 +
    1.33 +use "Concurrent/unsynchronized.ML";
    1.34 +val _ = PolyML.Compiler.forgetValue "ref";
    1.35 +val _ = PolyML.Compiler.forgetType "ref";
    1.36 +
    1.37 +
    1.38 +(* pervasive environment *)
    1.39 +
    1.40 +val _ = PolyML.Compiler.forgetValue "isSome";
    1.41 +val _ = PolyML.Compiler.forgetValue "getOpt";
    1.42 +val _ = PolyML.Compiler.forgetValue "valOf";
    1.43 +val _ = PolyML.Compiler.forgetValue "foldl";
    1.44 +val _ = PolyML.Compiler.forgetValue "foldr";
    1.45 +val _ = PolyML.Compiler.forgetValue "print";
    1.46 +val _ = PolyML.Compiler.forgetValue "explode";
    1.47 +val _ = PolyML.Compiler.forgetValue "concat";
    1.48 +
    1.49 +val ord = SML90.ord;
    1.50 +val chr = SML90.chr;
    1.51 +val raw_explode = SML90.explode;
    1.52 +val implode = SML90.implode;
    1.53 +
    1.54 +fun quit () = exit 0;
    1.55 +
    1.56 +
    1.57 +(* ML runtime system *)
    1.58 +
    1.59 +use "ML/ml_heap.ML";
    1.60 +use "ML/ml_profiling.ML";
    1.61 +
    1.62 +val pointer_eq = PolyML.pointerEq;
    1.63 +
    1.64 +
    1.65 +(* ML toplevel pretty printing *)
    1.66 +
    1.67 +use "ML/ml_pretty.ML";
    1.68 +
    1.69 +local
    1.70 +  val depth = Unsynchronized.ref 10;
    1.71 +in
    1.72 +  fun get_default_print_depth () = ! depth;
    1.73 +  fun default_print_depth n = (depth := n; PolyML.print_depth n);
    1.74 +  val _ = default_print_depth 10;
    1.75 +end;
    1.76 +
    1.77 +val error_depth = PolyML.error_depth;
    1.78 +
    1.79 +
    1.80 +(* ML compiler *)
    1.81 +
    1.82 +use "General/secure.ML";
    1.83 +use "ML/ml_compiler0.ML";
    1.84 +
    1.85 +PolyML.Compiler.reportUnreferencedIds := true;
    1.86 +PolyML.Compiler.reportExhaustiveHandlers := true;
    1.87 +PolyML.Compiler.printInAlphabeticalOrder := false;
    1.88 +PolyML.Compiler.maxInlineSize := 80;
    1.89 +PolyML.Compiler.prompt1 := "ML> ";
    1.90 +PolyML.Compiler.prompt2 := "ML# ";
    1.91 +
    1.92 +fun ml_make_string struct_name =
    1.93 +  "(fn x => Pretty.string_of (Pretty.from_ML (ML_Pretty.from_polyml (PolyML.prettyRepresentation (x, FixedInt.fromInt (" ^
    1.94 +    struct_name ^ ".ML_print_depth ()))))))";
    1.95 +
    1.96 +
    1.97 +(* ML debugger *)
    1.98 +
    1.99 +use_no_debug "ML/ml_debugger.ML";
   1.100 +
   1.101 +
   1.102 +
   1.103 +(** bootstrap phase 1: towards ML within position context *)
   1.104 +
   1.105  (* library of general tools *)
   1.106  
   1.107  use "General/basics.ML";
   1.108 @@ -52,7 +141,7 @@
   1.109  
   1.110  
   1.111  
   1.112 -(** bootstrap phase 1: towards ML within Isar context *)
   1.113 +(** bootstrap phase 2: towards ML within Isar context *)
   1.114  
   1.115  (* library of general tools *)
   1.116  
   1.117 @@ -236,7 +325,7 @@
   1.118  
   1.119  
   1.120  
   1.121 -(** bootstrap phase 2: towards Pure.thy and final ML toplevel setup *)
   1.122 +(** bootstrap phase 3: towards Pure.thy and final ML toplevel setup *)
   1.123  
   1.124  (*basic proof engine*)
   1.125  use "par_tactical.ML";