(* Title:  BaseDefinitions/thmC-def.sml

   Author: Walther Neuper

   (c) due to copyright terms

Probably this structure can be dropped due to improved reflection in Isabelle.

Here is a minimum of code required for theory Know_Store,

further code see structure ThmC.

*)

signature THEOREM_ISAC_DEF =

sig

  type T

  eqtype id

  val string_of_thm: thm -> string

  val string_of_thms: thm list -> string

(*stepwise replace ^^^ by vvv and finally rename by eliminating "_PIDE"*)

  val string_of_thm_PIDE: Proof.context -> thm -> string

  val string_of_thms_PIDE: Proof.context -> thm list -> string

(* required in ProgLang BEFORE definition in ---------------vvv   *)

  val int_opt_of_string: string -> int option (* belongs to TermC *)

end

(**)

structure ThmC_Def(**): THEOREM_ISAC_DEF(**) =

struct

(**)

type id = string; (* key into Know_Store, without point *)

type T = id * Thm.thm;

(*this is from times before the introduction of sessions*)

fun string_of_thm thm =

  let

    val t = Thm.prop_of thm

    val ctxt = Proof_Context.init_global (Thy_Info.get_theory ("Isac.Isac_Knowledge"))

    val ctxt' = Config.put show_markup false ctxt

  in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;

fun string_of_thms thms = (strs2str o (map (string_of_thm))) thms

fun string_of_thm_PIDE ctxt thm =

  let

    val t = Thm.prop_of thm

  (*val ctxt = Proof_Context.init_global (Thy_Info.get_theory ("Isac.Isac_Knowledge"))*)

    val ctxt' = Config.put show_markup false ctxt

  in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;

fun string_of_thms_PIDE ctxt thms = (strs2str o (map (string_of_thm_PIDE ctxt))) thms

fun int_opt_of_string str = 

  let

    val ss = Symbol.explode str

    val ss' = case ss of "(" :: s => drop_last s | _ => ss

    val (sign, istr) = case ss' of "-" :: istr => (~1, istr) | _ => (1, ss')

  in

    case Library.read_int istr of (i, []) => SOME (sign * i) | _ => NONE

  end;

(**)end(**)