theory Command
imports Main
keywords "foobar" "foobar_trace" :: thy_decl and
         "foobar_goal" "foobar_prove" :: thy_goal
begin

ML \<open>
let
   val do_nothing = Scan.succeed (Local_Theory.background_theory I)
in
   Outer_Syntax.local_theory @{command_spec "foobar"} 
     "description of foobar" 
       do_nothing
end
\<close>

ML \<open>
let
  fun trace_prop str =
     Local_Theory.background_theory (fn lthy => (tracing str; lthy))
  val trace_prop_parser = Parse.prop >> trace_prop
in
  Outer_Syntax.local_theory @{command_spec "foobar_trace"} 
    "traces a proposition"
      trace_prop_parser
end
\<close>

ML \<open>
let
   fun prove_prop str lthy =
     let
       val prop = Syntax.read_prop lthy str
     in
       Proof.theorem NONE (K I) [[(prop,[])]] lthy
     end;
   val prove_prop_parser = Parse.prop >> prove_prop
in
   Outer_Syntax.local_theory_to_proof @{command_spec "foobar_goal"} 
     "proving a proposition"
       prove_prop_parser
end
\<close>

ML \<open>
structure Result = Proof_Data(
  type T = unit -> term
  fun init thy () = error "Result")

val result_cookie = (Result.get, Result.put, "Result.put")
\<close>

ML\<open>
let
   fun after_qed thm_name thms lthy =
        Local_Theory.note (thm_name, (flat thms)) lthy |> snd

   fun setup_proof (thm_name, {text, ...}) lthy =
   let
     val trm = Code_Runtime.value lthy result_cookie ("", text)
   in
     Proof.theorem NONE (after_qed thm_name) [[(trm,[])]] lthy
   end

   val parser = Parse_Spec.opt_thm_name ":" -- Parse.ML_source
 
in
   Outer_Syntax.local_theory_to_proof @{command_spec "foobar_prove"} 
     "proving a proposition" 
        (parser >> setup_proof)
end\<close>




end