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
wenzelm@48879
     1
(*  Title:      Pure/pure_syn.ML
wenzelm@48879
     2
    Author:     Makarius
wenzelm@48879
     3
wenzelm@52546
     4
Minimal outer syntax for bootstrapping Isabelle/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@56204
    12
    (("theory", Keyword.tag_theory Keyword.thy_begin), @{here}) "begin theory"
wenzelm@48879
    13
    (Thy_Header.args >> (fn header =>
wenzelm@56895
    14
      Toplevel.init_theory
wenzelm@56895
    15
        (fn () => Thy_Info.toplevel_begin_theory (! ProofGeneral.master_path) header)));
wenzelm@48879
    16
wenzelm@48879
    17
val _ =
wenzelm@48879
    18
  Outer_Syntax.command
wenzelm@56204
    19
    (("ML_file", Keyword.tag_ml Keyword.thy_load), @{here}) "ML text from file"
wenzelm@56208
    20
    (Resources.parse_files "ML_file" >> (fn files => Toplevel.generic_theory (fn gthy =>
wenzelm@48879
    21
        let
wenzelm@55788
    22
          val [{src_path, lines, digest, pos}] = files (Context.theory_of gthy);
wenzelm@56208
    23
          val provide = Resources.provide (src_path, digest);
wenzelm@55828
    24
          val source = {delimited = true, text = cat_lines lines, pos = pos};
wenzelm@56618
    25
          val flags = {SML = false, exchange = false, redirect = true, verbose = true};
wenzelm@48879
    26
        in
wenzelm@48879
    27
          gthy
wenzelm@56304
    28
          |> ML_Context.exec (fn () => ML_Context.eval_source flags source)
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