| author | wenzelm | 
| Fri, 04 Apr 2014 12:07:48 +0200 | |
| changeset 56399 | 386e4cb7ad68 | 
| parent 56304 | 40274e4f5ebf | 
| child 56618 | 874bdedb2313 | 
| permissions | -rw-r--r-- | 
| 31333 
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
 wenzelm parents: diff
changeset | 1 | (* Title: Pure/ML/ml_compiler.ML | 
| 
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
 wenzelm parents: diff
changeset | 2 | Author: Makarius | 
| 
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
 wenzelm parents: diff
changeset | 3 | |
| 56303 
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
 wenzelm parents: 
56281diff
changeset | 4 | Runtime compilation and evaluation -- generic version. | 
| 31333 
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
 wenzelm parents: diff
changeset | 5 | *) | 
| 
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
 wenzelm parents: diff
changeset | 6 | |
| 
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
 wenzelm parents: diff
changeset | 7 | signature ML_COMPILER = | 
| 
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
 wenzelm parents: diff
changeset | 8 | sig | 
| 56304 
40274e4f5ebf
redirect ML_Compiler reports more directly: only the (big) parse tree report is deferred via Execution.print (NB: this does not work for asynchronous "diag" commands);
 wenzelm parents: 
56303diff
changeset | 9 |   type flags = {SML: bool, redirect: bool, verbose: bool}
 | 
| 
40274e4f5ebf
redirect ML_Compiler reports more directly: only the (big) parse tree report is deferred via Execution.print (NB: this does not work for asynchronous "diag" commands);
 wenzelm parents: 
56303diff
changeset | 10 | val flags: flags | 
| 
40274e4f5ebf
redirect ML_Compiler reports more directly: only the (big) parse tree report is deferred via Execution.print (NB: this does not work for asynchronous "diag" commands);
 wenzelm parents: 
56303diff
changeset | 11 | val verbose: bool -> flags -> flags | 
| 56275 
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
 wenzelm parents: 
54387diff
changeset | 12 | val eval: flags -> Position.T -> ML_Lex.token list -> unit | 
| 31333 
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
 wenzelm parents: diff
changeset | 13 | end | 
| 
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
 wenzelm parents: diff
changeset | 14 | |
| 
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
 wenzelm parents: diff
changeset | 15 | structure ML_Compiler: ML_COMPILER = | 
| 
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
 wenzelm parents: diff
changeset | 16 | struct | 
| 
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
 wenzelm parents: diff
changeset | 17 | |
| 56304 
40274e4f5ebf
redirect ML_Compiler reports more directly: only the (big) parse tree report is deferred via Execution.print (NB: this does not work for asynchronous "diag" commands);
 wenzelm parents: 
56303diff
changeset | 18 | type flags = {SML: bool, redirect: bool, verbose: bool};
 | 
| 
40274e4f5ebf
redirect ML_Compiler reports more directly: only the (big) parse tree report is deferred via Execution.print (NB: this does not work for asynchronous "diag" commands);
 wenzelm parents: 
56303diff
changeset | 19 | val flags = {SML = false, redirect = false, verbose = false};
 | 
| 
40274e4f5ebf
redirect ML_Compiler reports more directly: only the (big) parse tree report is deferred via Execution.print (NB: this does not work for asynchronous "diag" commands);
 wenzelm parents: 
56303diff
changeset | 20 | fun verbose v (flags: flags) = {SML = #SML flags, redirect = #redirect flags, verbose = v};
 | 
| 56275 
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
 wenzelm parents: 
54387diff
changeset | 21 | |
| 56304 
40274e4f5ebf
redirect ML_Compiler reports more directly: only the (big) parse tree report is deferred via Execution.print (NB: this does not work for asynchronous "diag" commands);
 wenzelm parents: 
56303diff
changeset | 22 | fun eval (flags: flags) pos toks = | 
| 31333 
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
 wenzelm parents: diff
changeset | 23 | let | 
| 56304 
40274e4f5ebf
redirect ML_Compiler reports more directly: only the (big) parse tree report is deferred via Execution.print (NB: this does not work for asynchronous "diag" commands);
 wenzelm parents: 
56303diff
changeset | 24 |     val _ = if #SML flags then error ("Standard ML is unsupported on " ^ ML_System.name) else ();
 | 
| 31333 
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
 wenzelm parents: diff
changeset | 25 | val line = the_default 1 (Position.line_of pos); | 
| 
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
 wenzelm parents: diff
changeset | 26 | val file = the_default "ML" (Position.file_of pos); | 
| 
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
 wenzelm parents: diff
changeset | 27 | val text = ML_Lex.flatten toks; | 
| 56304 
40274e4f5ebf
redirect ML_Compiler reports more directly: only the (big) parse tree report is deferred via Execution.print (NB: this does not work for asynchronous "diag" commands);
 wenzelm parents: 
56303diff
changeset | 28 | in Secure.use_text ML_Env.local_context (line, file) (#verbose flags) text end; | 
| 31333 
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
 wenzelm parents: diff
changeset | 29 | |
| 
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
 wenzelm parents: diff
changeset | 30 | end; | 
| 
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
 wenzelm parents: diff
changeset | 31 |