clarified modules;
authorwenzelm
Sat Apr 02 20:23:51 2016 +0200 (2016-04-02)
changeset 62817744bfd770123
parent 62816 19387866eace
child 62818 2733b240bfea
clarified modules;
src/Pure/ML/ml_compiler0.ML
src/Pure/ML/ml_compiler1.ML
src/Pure/ML/ml_compiler2.ML
src/Pure/ROOT
src/Pure/ROOT.ML
     1.1 --- a/src/Pure/ML/ml_compiler0.ML	Sat Apr 02 17:11:27 2016 +0200
     1.2 +++ b/src/Pure/ML/ml_compiler0.ML	Sat Apr 02 20:23:51 2016 +0200
     1.3 @@ -1,7 +1,8 @@
     1.4  (*  Title:      Pure/ML/ml_compiler0.ML
     1.5 +    Author:     Makarius
     1.6  
     1.7 -Runtime compilation and evaluation (bootstrap version of
     1.8 -Pure/ML/ml_compiler.ML).
     1.9 +Runtime compilation and evaluation for bootstrap.
    1.10 +Initial ML use operations.
    1.11  *)
    1.12  
    1.13  signature ML_COMPILER0 =
    1.14 @@ -12,6 +13,7 @@
    1.15      here: int -> string -> string,
    1.16      print: string -> unit,
    1.17      error: string -> unit}
    1.18 +  val make_context: ML_Name_Space.T -> context
    1.19    val use_text: context -> {debug: bool, file: string, line: int, verbose: bool} -> string -> unit
    1.20    val use_file: context -> {debug: bool, verbose: bool} -> string -> unit
    1.21    val debug_option: bool option -> bool
    1.22 @@ -22,6 +24,16 @@
    1.23  structure ML_Compiler0: ML_COMPILER0 =
    1.24  struct
    1.25  
    1.26 +(* global options *)
    1.27 +
    1.28 +val _ = PolyML.Compiler.reportUnreferencedIds := true;
    1.29 +val _ = PolyML.Compiler.reportExhaustiveHandlers := true;
    1.30 +val _ = PolyML.Compiler.printInAlphabeticalOrder := false;
    1.31 +val _ = PolyML.Compiler.maxInlineSize := 80;
    1.32 +
    1.33 +
    1.34 +(* context *)
    1.35 +
    1.36  type context =
    1.37   {name_space: ML_Name_Space.T,
    1.38    print_depth: int option,
    1.39 @@ -29,6 +41,18 @@
    1.40    print: string -> unit,
    1.41    error: string -> unit};
    1.42  
    1.43 +fun make_context name_space : context =
    1.44 + {name_space = name_space,
    1.45 +  print_depth = NONE,
    1.46 +  here = fn line => fn file => " (line " ^ Int.toString line ^ " of \"" ^ file ^ "\")",
    1.47 +  print = fn s => (TextIO.output (TextIO.stdOut, s ^ "\n"); TextIO.flushOut TextIO.stdOut),
    1.48 +  error = fn s => error s};
    1.49 +
    1.50 +
    1.51 +(* use operations *)
    1.52 +
    1.53 +local
    1.54 +
    1.55  fun drop_newline s =
    1.56    if String.isSuffix "\n" s then String.substring (s, 0, size s - 1)
    1.57    else s;
    1.58 @@ -47,6 +71,8 @@
    1.59        | input _ [] res = rev res;
    1.60    in String.concat (input start_line (String.explode txt) []) end;
    1.61  
    1.62 +in
    1.63 +
    1.64  fun use_text ({name_space, print_depth, here, print, error, ...}: context)
    1.65      {line, file, verbose, debug} text =
    1.66    let
    1.67 @@ -86,30 +112,28 @@
    1.68            error (output ()); Exn.reraise exn);
    1.69    in if verbose then print (output ()) else () end;
    1.70  
    1.71 +end;
    1.72 +
    1.73  fun use_file context {verbose, debug} file =
    1.74    let
    1.75      val instream = TextIO.openIn file;
    1.76      val text = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
    1.77    in use_text context {line = 1, file = file, verbose = verbose, debug = debug} text end;
    1.78  
    1.79 +fun use_operations (use_ : bool option -> string -> unit) =
    1.80 +  {use = use_ NONE, use_debug = use_ (SOME true), use_no_debug = use_ (SOME false)};
    1.81 +
    1.82  
    1.83  fun debug_option NONE = OS.Process.getEnv "ISABELLE_ML_DEBUGGER" = SOME "true"
    1.84    | debug_option (SOME debug) = debug;
    1.85  
    1.86 -fun use_operations (use_ : bool option -> string -> unit) =
    1.87 -  {use = use_ NONE, use_debug = use_ (SOME true), use_no_debug = use_ (SOME false)};
    1.88 +end;
    1.89  
    1.90 -end;
    1.91 +
    1.92 +(* initial use operations *)
    1.93  
    1.94  val {use, use_debug, use_no_debug} =
    1.95 -  let
    1.96 -    val context: ML_Compiler0.context =
    1.97 -     {name_space = ML_Name_Space.global,
    1.98 -      print_depth = NONE,
    1.99 -      here = fn line => fn file => " (line " ^ Int.toString line ^ " of \"" ^ file ^ "\")",
   1.100 -      print = fn s => (TextIO.output (TextIO.stdOut, s ^ "\n"); TextIO.flushOut TextIO.stdOut),
   1.101 -      error = fn s => error s};
   1.102 -  in
   1.103 +  let val context = ML_Compiler0.make_context ML_Name_Space.global in
   1.104      ML_Compiler0.use_operations (fn opt_debug => fn file =>
   1.105        ML_Compiler0.use_file context
   1.106          {verbose = true, debug = ML_Compiler0.debug_option opt_debug} file
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/Pure/ML/ml_compiler1.ML	Sat Apr 02 20:23:51 2016 +0200
     2.3 @@ -0,0 +1,22 @@
     2.4 +(*  Title:      Pure/ML/ml_compiler1.ML
     2.5 +    Author:     Makarius
     2.6 +
     2.7 +Refined ML use operations for bootstrap.
     2.8 +*)
     2.9 +
    2.10 +val {use, use_debug, use_no_debug} =
    2.11 +  let
    2.12 +    val context: ML_Compiler0.context =
    2.13 +     {name_space = ML_Name_Space.global,
    2.14 +      print_depth = NONE,
    2.15 +      here = Position.here oo Position.line_file,
    2.16 +      print = writeln,
    2.17 +      error = error};
    2.18 +  in
    2.19 +    ML_Compiler0.use_operations (fn opt_debug => fn file =>
    2.20 +      Position.setmp_thread_data (Position.file_only file)
    2.21 +        (fn () =>
    2.22 +          ML_Compiler0.use_file context
    2.23 +            {verbose = true, debug = ML_Compiler0.debug_option opt_debug} file
    2.24 +          handle ERROR msg => (writeln msg; error "ML error")) ())
    2.25 +  end;
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Pure/ML/ml_compiler2.ML	Sat Apr 02 20:23:51 2016 +0200
     3.3 @@ -0,0 +1,12 @@
     3.4 +(*  Title:      Pure/ML/ml_compiler2.ML
     3.5 +    Author:     Makarius
     3.6 +
     3.7 +Isabelle/ML use operations.
     3.8 +*)
     3.9 +
    3.10 +val {use, use_debug, use_no_debug} =
    3.11 +  ML_Compiler0.use_operations (fn opt_debug => fn file =>
    3.12 +    let val flags = ML_Compiler.verbose true (ML_Compiler.debug_flags opt_debug) in
    3.13 +      ML_Context.eval_file flags (Path.explode file)
    3.14 +        handle ERROR msg => (writeln msg; error "ML error")
    3.15 +    end);
     4.1 --- a/src/Pure/ROOT	Sat Apr 02 17:11:27 2016 +0200
     4.2 +++ b/src/Pure/ROOT	Sat Apr 02 20:23:51 2016 +0200
     4.3 @@ -101,6 +101,8 @@
     4.4      "ML/ml_antiquotation.ML"
     4.5      "ML/ml_compiler.ML"
     4.6      "ML/ml_compiler0.ML"
     4.7 +    "ML/ml_compiler1.ML"
     4.8 +    "ML/ml_compiler2.ML"
     4.9      "ML/ml_context.ML"
    4.10      "ML/ml_debugger.ML"
    4.11      "ML/ml_env.ML"
     5.1 --- a/src/Pure/ROOT.ML	Sat Apr 02 17:11:27 2016 +0200
     5.2 +++ b/src/Pure/ROOT.ML	Sat Apr 02 20:23:51 2016 +0200
     5.3 @@ -63,11 +63,6 @@
     5.4  
     5.5  use "ML/ml_compiler0.ML";
     5.6  
     5.7 -PolyML.Compiler.reportUnreferencedIds := true;
     5.8 -PolyML.Compiler.reportExhaustiveHandlers := true;
     5.9 -PolyML.Compiler.printInAlphabeticalOrder := false;
    5.10 -PolyML.Compiler.maxInlineSize := 80;
    5.11 -
    5.12  
    5.13  (* ML debugger *)
    5.14  
    5.15 @@ -100,24 +95,7 @@
    5.16  use "General/input.ML";
    5.17  use "General/antiquote.ML";
    5.18  use "ML/ml_lex.ML";
    5.19 -
    5.20 -val {use, use_debug, use_no_debug} =
    5.21 -  let
    5.22 -    val context: ML_Compiler0.context =
    5.23 -     {name_space = ML_Name_Space.global,
    5.24 -      print_depth = NONE,
    5.25 -      here = Position.here oo Position.line_file,
    5.26 -      print = writeln,
    5.27 -      error = error};
    5.28 -  in
    5.29 -    ML_Compiler0.use_operations (fn opt_debug => fn file =>
    5.30 -      Position.setmp_thread_data (Position.file_only file)
    5.31 -        (fn () =>
    5.32 -          ML_Compiler0.use_file context
    5.33 -            {verbose = true, debug = ML_Compiler0.debug_option opt_debug} file
    5.34 -          handle ERROR msg => (writeln msg; error "ML error")) ())
    5.35 -  end;
    5.36 -
    5.37 +use "ML/ml_compiler1.ML";
    5.38  
    5.39  
    5.40  (** bootstrap phase 2: towards ML within Isar context *)
    5.41 @@ -287,13 +265,7 @@
    5.42  (*ML with context and antiquotations*)
    5.43  use "ML/ml_context.ML";
    5.44  use "ML/ml_antiquotation.ML";
    5.45 -
    5.46 -val {use, use_debug, use_no_debug} =
    5.47 -  ML_Compiler0.use_operations (fn opt_debug => fn file =>
    5.48 -    let val flags = ML_Compiler.verbose true (ML_Compiler.debug_flags opt_debug) in
    5.49 -      ML_Context.eval_file flags (Path.explode file)
    5.50 -        handle ERROR msg => (writeln msg; error "ML error")
    5.51 -    end);
    5.52 +use "ML/ml_compiler2.ML";
    5.53  
    5.54  
    5.55