1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/libisabelle-protocol/classy/Classy.thy	Tue Sep 04 14:50:30 2018 +0200
     1.3 @@ -0,0 +1,35 @@
     1.4 +theory Classy
     1.5 +imports Pure
     1.6 +keywords
     1.7 +  "ML.class" :: thy_decl % "ML" and
     1.8 +  "ML.instance" :: thy_decl % "ML" and
     1.9 +  "ML.print_classes" :: diag
    1.10 +begin
    1.11 +
    1.12 +(* FIXME unfold in ML files *)
    1.13 +ML\<open>
    1.14 +  val secure_use_text = ML_Compiler0.ML
    1.15 +  val context_set_thread_data = Context.setmp_generic_context
    1.16 +  fun ml_env_context return : ML_Compiler0.context =
    1.17 +    {name_space = #name_space ML_Env.context,
    1.18 +     print_depth = SOME 1000000,
    1.19 +     here = #here ML_Env.context,
    1.20 +     print = fn r => return := SOME r,
    1.21 +     error = #error ML_Env.context}
    1.22 +  val print_int = Value.print_int
    1.23 +\<close>
    1.24 +
    1.25 +ML_file "ml_types.ML"
    1.26 +ML_file "classy.ML"
    1.27 +
    1.28 +setup \<open>Classy.setup\<close>
    1.29 +
    1.30 +ML_file "pretty_class.ML"
    1.31 +
    1.32 +ML.class pretty = \<open>'a pretty_class\<close>
    1.33 +
    1.34 +ML.instance \<open>Pretty_Class.string\<close> :: pretty
    1.35 +ML.instance \<open>Pretty_Class.pretty\<close> :: pretty
    1.36 +ML.instance \<open>Pretty_Class.list\<close> :: pretty
    1.37 +
    1.38 +end