CookBook/Base.thy
author Christian Urban <urbanc@in.tum.de>
Tue, 17 Mar 2009 17:32:12 +0100
changeset 183 8bb4eaa2ec92
parent 161 83f36a1c62f2
permissions -rw-r--r--
a simplification suggested by Stefan and some polishing

theory Base
imports Main
uses
  "chunks.ML"
  "antiquote_setup.ML"
begin

(* to have a special tag for text enclosed in ML *)
ML {*

val _ =
  OuterSyntax.command "ML" "eval ML text within theory"
    (OuterKeyword.tag "TutorialML" OuterKeyword.thy_decl)
    (OuterParse.ML_source >> (fn (txt, pos) =>
      Toplevel.generic_theory (ML_Context.exec (fn () => ML_Context.eval true pos txt))));
*}
(*
ML {*
  fun warning str = str
  fun tracing str = str
*}
*)
end