src/Pure/pure_syn.ML

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";

(*  Title:      Pure/pure_syn.ML
    Author:     Makarius

Minimal outer syntax for bootstrapping Isabelle/Pure.
*)

structure Pure_Syn: sig end =
struct

val _ =
  Outer_Syntax.command
    (("theory", Keyword.tag_theory Keyword.thy_begin), Position.file "pure_syn.ML")
    "begin theory context"
    (Thy_Header.args >> (fn header =>
      Toplevel.print o
        Toplevel.init_theory
          (fn () => Thy_Info.toplevel_begin_theory (! ProofGeneral.master_path) header)));

val _ =
  Outer_Syntax.command
    (("ML_file", Keyword.tag_ml Keyword.thy_load), Position.file "pure_syn.ML")
    "ML text from file"
    (Thy_Load.parse_files "ML_file" >> (fn files => Toplevel.generic_theory (fn gthy =>
        let
          val [{src_path, lines, digest, pos}] = files (Context.theory_of gthy);
          val provide = Thy_Load.provide (src_path, digest);
          val source = {delimited = true, text = cat_lines lines, pos = pos};
        in
          gthy
          |> ML_Context.exec (fn () => ML_Context.eval_source true source)
          |> Local_Theory.propagate_ml_env
          |> Context.mapping provide (Local_Theory.background_theory provide)
        end)));

end;