src/Pure/pure_syn.ML
author wenzelm
Sat, 01 Mar 2014 22:46:31 +0100
changeset 55828 42ac3cfb89f6
parent 55788 67699e08e969
child 56204 f70e69208a8c
permissions -rw-r--r--
clarified language markup: added "delimited" property; type Symbol_Pos.source preserves information about delimited outer tokens (e.g string, cartouche); observe Completion.Language_Context only for delimited languages, which is important to complete keywords after undelimited inner tokens, e.g. "lemma A pro";
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
54450
7815563f50dc tuned signature -- clarified Proof General legacy;
wenzelm
parents: 52546
diff changeset
    17
          (fn () => Thy_Info.toplevel_begin_theory (! ProofGeneral.master_path) header)));
48879
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
55788
67699e08e969 store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing;
wenzelm
parents: 54450
diff changeset
    25
          val [{src_path, lines, digest, pos}] = files (Context.theory_of gthy);
67699e08e969 store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing;
wenzelm
parents: 54450
diff changeset
    26
          val provide = Thy_Load.provide (src_path, digest);
55828
42ac3cfb89f6 clarified language markup: added "delimited" property;
wenzelm
parents: 55788
diff changeset
    27
          val source = {delimited = true, text = cat_lines lines, pos = pos};
48879
cb5cdbb645cd clarified bootstrapping of Pure;
wenzelm
parents:
diff changeset
    28
        in
cb5cdbb645cd clarified bootstrapping of Pure;
wenzelm
parents:
diff changeset
    29
          gthy
55828
42ac3cfb89f6 clarified language markup: added "delimited" property;
wenzelm
parents: 55788
diff changeset
    30
          |> ML_Context.exec (fn () => ML_Context.eval_source true source)
48879
cb5cdbb645cd clarified bootstrapping of Pure;
wenzelm
parents:
diff changeset
    31
          |> Local_Theory.propagate_ml_env
cb5cdbb645cd clarified bootstrapping of Pure;
wenzelm
parents:
diff changeset
    32
          |> Context.mapping provide (Local_Theory.background_theory provide)
cb5cdbb645cd clarified bootstrapping of Pure;
wenzelm
parents:
diff changeset
    33
        end)));
cb5cdbb645cd clarified bootstrapping of Pure;
wenzelm
parents:
diff changeset
    34
cb5cdbb645cd clarified bootstrapping of Pure;
wenzelm
parents:
diff changeset
    35
end;
cb5cdbb645cd clarified bootstrapping of Pure;
wenzelm
parents:
diff changeset
    36