theory Test_Input
  imports Main
  keywords "Input_Test" :: thy_decl
begin
ML \<open>
datatype probably_empty = Empty of term * string | Term of term

structure Data = Theory_Data
(
  type T = probably_empty option;
  val empty = NONE;
  fun merge _ = NONE;
);
val set_data = Data.put o SOME;
fun the_data thy = 
  case Data.get thy of NONE => Term @{term empty}
  | SOME probably_empty => probably_empty;

fun is_empty_dummy "[__=__, __=__]" = true
  | is_empty_dummy _ = false

fun split_descriptor_dummy str =
  (implode (take 9 (Symbol.explode str)), implode (drop 10 (Symbol.explode str)))
(*test*)val ("Constants", "[__=__, __=__]") = split_descriptor_dummy "Constants [__=__, __=__]";

fun parse_term thy (str, pos) =
  let
    val ctxt = Proof_Context.init_global thy
    val (descr, arg) = split_descriptor_dummy str
  in
    if is_empty_dummy arg
    then Empty (Syntax.read_term ctxt descr
      handle ERROR msg => error (msg ^ Position.here pos), arg)
    else Term (Syntax.read_term ctxt str
        handle ERROR msg => error (msg ^ Position.here pos))
  end

val _ =
  Outer_Syntax.command \<^command_keyword>\<open>Input_Test\<close>
    "Malformed YXML: unbalanced element \"inpu\""
    ((Parse.position Parse.term) >>
      (fn (str, pos) =>
        Toplevel.theory (fn thy =>
          let val store = parse_term thy (str, pos)
          in set_data store thy end) ))
\<close>

Input_Test \<open>Constants [__=__, __=__]\<close>
Input_Test \<open>Constants [r = 7]\<close>

ML \<open>
(*/---------------------------------------- mimic input from PIDE -----------------------------\*)
val thy = @{theory}
val (str, pos) = ("Constants [__=__, __=__]", Position.none)
(*\---------------------------------------- mimic input from PIDE -----------------------------/*)
    val ctxt = Proof_Context.init_global thy
    val (descr, arg) = split_descriptor_dummy str;
    (*if*) is_empty_dummy arg (*true*);
(*test*)val Empty (Free ("Constants", _), "[__=__, __=__]") = Empty (Syntax.read_term ctxt descr, arg)
\<close>
end