src/Pure/pure_syn.ML
author wenzelm
Sun, 07 Jul 2013 17:30:16 +0200
changeset 52546 7118524a2a24
parent 52455 9a8f4fdac3cf
child 54450 7815563f50dc
permissions -rw-r--r--
tuned comments;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
48879
cb5cdbb645cd clarified bootstrapping of Pure;
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/pure_syn.ML
cb5cdbb645cd clarified bootstrapping of Pure;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
cb5cdbb645cd clarified bootstrapping of Pure;
wenzelm
parents:
diff changeset
     3
52546
7118524a2a24 tuned comments;
wenzelm
parents: 52455
diff changeset
     4
Minimal outer syntax for bootstrapping Isabelle/Pure.
48879
cb5cdbb645cd clarified bootstrapping of Pure;
wenzelm
parents:
diff changeset
     5
*)
cb5cdbb645cd clarified bootstrapping of Pure;
wenzelm
parents:
diff changeset
     6
cb5cdbb645cd clarified bootstrapping of Pure;
wenzelm
parents:
diff changeset
     7
structure Pure_Syn: sig end =
cb5cdbb645cd clarified bootstrapping of Pure;
wenzelm
parents:
diff changeset
     8
struct
cb5cdbb645cd clarified bootstrapping of Pure;
wenzelm
parents:
diff changeset
     9
cb5cdbb645cd clarified bootstrapping of Pure;
wenzelm
parents:
diff changeset
    10
val _ =
cb5cdbb645cd clarified bootstrapping of Pure;
wenzelm
parents:
diff changeset
    11
  Outer_Syntax.command
52455
9a8f4fdac3cf more position information for markup;
wenzelm
parents: 48905
diff changeset
    12
    (("theory", Keyword.tag_theory Keyword.thy_begin), Position.file "pure_syn.ML")
9a8f4fdac3cf more position information for markup;
wenzelm
parents: 48905
diff changeset
    13
    "begin theory context"
48879
cb5cdbb645cd clarified bootstrapping of Pure;
wenzelm
parents:
diff changeset
    14
    (Thy_Header.args >> (fn header =>
cb5cdbb645cd clarified bootstrapping of Pure;
wenzelm
parents:
diff changeset
    15
      Toplevel.print o
cb5cdbb645cd clarified bootstrapping of Pure;
wenzelm
parents:
diff changeset
    16
        Toplevel.init_theory
cb5cdbb645cd clarified bootstrapping of Pure;
wenzelm
parents:
diff changeset
    17
          (fn () => Thy_Info.toplevel_begin_theory (Thy_Load.get_master_path ()) header)));
cb5cdbb645cd clarified bootstrapping of Pure;
wenzelm
parents:
diff changeset
    18
cb5cdbb645cd clarified bootstrapping of Pure;
wenzelm
parents:
diff changeset
    19
val _ =
cb5cdbb645cd clarified bootstrapping of Pure;
wenzelm
parents:
diff changeset
    20
  Outer_Syntax.command
52455
9a8f4fdac3cf more position information for markup;
wenzelm
parents: 48905
diff changeset
    21
    (("ML_file", Keyword.tag_ml Keyword.thy_load), Position.file "pure_syn.ML")
9a8f4fdac3cf more position information for markup;
wenzelm
parents: 48905
diff changeset
    22
    "ML text from file"
48905
04576657cf94 clarified type Token.file;
wenzelm
parents: 48896
diff changeset
    23
    (Thy_Load.parse_files "ML_file" >> (fn files => Toplevel.generic_theory (fn gthy =>
48879
cb5cdbb645cd clarified bootstrapping of Pure;
wenzelm
parents:
diff changeset
    24
        let
48905
04576657cf94 clarified type Token.file;
wenzelm
parents: 48896
diff changeset
    25
          val [{src_path, text, pos}] = files (Context.theory_of gthy);
04576657cf94 clarified type Token.file;
wenzelm
parents: 48896
diff changeset
    26
          val provide = Thy_Load.provide (src_path, SHA1.digest text);
48879
cb5cdbb645cd clarified bootstrapping of Pure;
wenzelm
parents:
diff changeset
    27
        in
cb5cdbb645cd clarified bootstrapping of Pure;
wenzelm
parents:
diff changeset
    28
          gthy
48905
04576657cf94 clarified type Token.file;
wenzelm
parents: 48896
diff changeset
    29
          |> ML_Context.exec (fn () => ML_Context.eval_text true pos text)
48879
cb5cdbb645cd clarified bootstrapping of Pure;
wenzelm
parents:
diff changeset
    30
          |> Local_Theory.propagate_ml_env
cb5cdbb645cd clarified bootstrapping of Pure;
wenzelm
parents:
diff changeset
    31
          |> Context.mapping provide (Local_Theory.background_theory provide)
cb5cdbb645cd clarified bootstrapping of Pure;
wenzelm
parents:
diff changeset
    32
        end)));
cb5cdbb645cd clarified bootstrapping of Pure;
wenzelm
parents:
diff changeset
    33
cb5cdbb645cd clarified bootstrapping of Pure;
wenzelm
parents:
diff changeset
    34
end;
cb5cdbb645cd clarified bootstrapping of Pure;
wenzelm
parents:
diff changeset
    35