(* Title:  "BridgeJEdit/preliminary.sml"

   Author: Walther Neuper

   (c) due to copyright terms

*)

"-----------------------------------------------------------------------------------------------";

"table of contents -----------------------------------------------------------------------------";

"-----------------------------------------------------------------------------------------------";

"----------- investigate Pure/context.ML THEORY_DATA -------------------------------------------";

"-----------------------------------------------------------------------------------------------";

"-----------------------------------------------------------------------------------------------";

"-----------------------------------------------------------------------------------------------";

"----------- investigate Pure/context.ML THEORY_DATA -------------------------------------------";

"----------- investigate Pure/context.ML THEORY_DATA -------------------------------------------";

"----------- investigate Pure/context.ML THEORY_DATA -------------------------------------------";

(* Pure/context.ML

signature THEORY_DATA =

sig

  type T

  val get: theory -> T

  val put: T -> theory -> theory

  val map: (T -> T) -> theory -> theory

end;*)

(*

Refs_Data.empty;                                    (*in Refs_Data defined workers are hidden*)

Refs_Data.extend;                                   (*in Refs_Data defined workers are hidden*)

Refs_Data.merge;                                    (*in Refs_Data defined workers are hidden*)

ML error:

Value or constructor (empty) has not been declared in structure Refs *)

Refs_Data.get: theory -> Refs_Data.T;                            (*from signature THEORY_DATA*)

Refs_Data.put: Refs_Data.T -> theory -> theory;                  (*from signature THEORY_DATA*)

Refs_Data.map: (Refs_Data.T -> Refs_Data.T) -> theory -> theory; (*from signature THEORY_DATA*)