src/Pure/pure_syn.ML
author wenzelm
Fri Apr 12 14:54:14 2013 +0200 (2013-04-12)
changeset 51700 c8f2bad67dbb
parent 48905 04576657cf94
child 52455 9a8f4fdac3cf
permissions -rw-r--r--
tuned signature;
tuned comments;
     1 (*  Title:      Pure/pure_syn.ML
     2     Author:     Makarius
     3 
     4 Minimal outer syntax for bootstrapping 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), Position.none) "begin theory context"
    13     (Thy_Header.args >> (fn header =>
    14       Toplevel.print o
    15         Toplevel.init_theory
    16           (fn () => Thy_Info.toplevel_begin_theory (Thy_Load.get_master_path ()) header)));
    17 
    18 val _ =
    19   Outer_Syntax.command
    20     (("ML_file", Keyword.tag_ml Keyword.thy_load), Position.none) "ML text from file"
    21     (Thy_Load.parse_files "ML_file" >> (fn files => Toplevel.generic_theory (fn gthy =>
    22         let
    23           val [{src_path, text, pos}] = files (Context.theory_of gthy);
    24           val provide = Thy_Load.provide (src_path, SHA1.digest text);
    25         in
    26           gthy
    27           |> ML_Context.exec (fn () => ML_Context.eval_text true pos text)
    28           |> Local_Theory.propagate_ml_env
    29           |> Context.mapping provide (Local_Theory.background_theory provide)
    30         end)));
    31 
    32 end;
    33