src/Pure/pure_syn.ML
author blanchet
Mon May 19 23:43:53 2014 +0200 (2014-05-19)
changeset 57008 10f68b83b474
parent 56895 f058120aaad4
child 58842 22b87ab47d3b
permissions -rw-r--r--
use E 1.8's auto scheduler option
     1 (*  Title:      Pure/pure_syn.ML
     2     Author:     Makarius
     3 
     4 Minimal outer syntax for bootstrapping Isabelle/Pure.
     5 *)
     6 
     7 structure Pure_Syn: sig end =
     8 struct
     9 
    10 val _ =
    11   Outer_Syntax.command
    12     (("theory", Keyword.tag_theory Keyword.thy_begin), @{here}) "begin theory"
    13     (Thy_Header.args >> (fn header =>
    14       Toplevel.init_theory
    15         (fn () => Thy_Info.toplevel_begin_theory (! ProofGeneral.master_path) header)));
    16 
    17 val _ =
    18   Outer_Syntax.command
    19     (("ML_file", Keyword.tag_ml Keyword.thy_load), @{here}) "ML text from file"
    20     (Resources.parse_files "ML_file" >> (fn files => Toplevel.generic_theory (fn gthy =>
    21         let
    22           val [{src_path, lines, digest, pos}] = files (Context.theory_of gthy);
    23           val provide = Resources.provide (src_path, digest);
    24           val source = {delimited = true, text = cat_lines lines, pos = pos};
    25           val flags = {SML = false, exchange = false, redirect = true, verbose = true};
    26         in
    27           gthy
    28           |> ML_Context.exec (fn () => ML_Context.eval_source flags source)
    29           |> Local_Theory.propagate_ml_env
    30           |> Context.mapping provide (Local_Theory.background_theory provide)
    31         end)));
    32 
    33 end;
    34