src/Pure/pure_syn.ML
author wenzelm
Wed Aug 22 12:07:11 2012 +0200 (2012-08-22 ago)
changeset 48879 cb5cdbb645cd
child 48881 46e053eda5dd
permissions -rw-r--r--
clarified bootstrapping of Pure;
wenzelm@48879
     1
(*  Title:      Pure/pure_syn.ML
wenzelm@48879
     2
    Author:     Makarius
wenzelm@48879
     3
wenzelm@48879
     4
Minimal outer syntax for bootstrapping Pure.
wenzelm@48879
     5
*)
wenzelm@48879
     6
wenzelm@48879
     7
structure Pure_Syn: sig end =
wenzelm@48879
     8
struct
wenzelm@48879
     9
wenzelm@48879
    10
val _ =
wenzelm@48879
    11
  Outer_Syntax.command
wenzelm@48879
    12
    (("theory", Keyword.tag_theory Keyword.thy_begin), Position.none) "begin theory context"
wenzelm@48879
    13
    (Thy_Header.args >> (fn header =>
wenzelm@48879
    14
      Toplevel.print o
wenzelm@48879
    15
        Toplevel.init_theory
wenzelm@48879
    16
          (fn () => Thy_Info.toplevel_begin_theory (Thy_Load.get_master_path ()) header)));
wenzelm@48879
    17
wenzelm@48879
    18
val _ =
wenzelm@48879
    19
  Outer_Syntax.command
wenzelm@48879
    20
    (("ML_file", Keyword.tag_ml Keyword.thy_load), Position.none) "ML text from file"
wenzelm@48879
    21
    (Scan.ahead Parse.path -- Thy_Load.parse_files "ML_file"
wenzelm@48879
    22
      >> (fn (src_path, files) => Toplevel.generic_theory (fn gthy =>
wenzelm@48879
    23
        let
wenzelm@48879
    24
          val (dir, [(txt, pos)]) = files (Context.theory_of gthy);
wenzelm@48879
    25
          val provide = Thy_Load.provide (src_path, (File.full_path dir src_path, SHA1.digest txt));
wenzelm@48879
    26
        in
wenzelm@48879
    27
          gthy
wenzelm@48879
    28
          |> ML_Context.exec (fn () => ML_Context.eval_text true pos txt)
wenzelm@48879
    29
          |> Local_Theory.propagate_ml_env
wenzelm@48879
    30
          |> Context.mapping provide (Local_Theory.background_theory provide)
wenzelm@48879
    31
        end)));
wenzelm@48879
    32
wenzelm@48879
    33
end;
wenzelm@48879
    34