(* Title:  BaseDefinitions/tracing.sml

   Author: Walther Neuper

   (c) due to copyright terms

This structure could be dropped due to improved reflection in Isabelle;

but ThmC.sym_thm requires still an identifying string thm_id.

*)

signature TRACING =

sig

(*/------- to Trace from Celem -------\*)

    val trace_calc: bool Unsynchronized.ref

    val trace_rewrite: bool Unsynchronized.ref

(*\------- to Trace from Celem --------/*)

(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)

  (*NONE*)

(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )

  (*NONE*)

( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)

end

(**)

structure Trace(**): TRACING(**) =

struct

(**)

(*/------- to Trace from Celem -------\*)

(* trace internal steps of isac's numeral calculations *)

val trace_calc = Unsynchronized.ref false;

(* trace internal steps of isac's rewriter *)

val trace_rewrite = Unsynchronized.ref false;

(* depth of recursion in traces of the rewriter, if trace_rewrite:=true *)

val depth = Unsynchronized.ref 99999;

(* no of rewrites exceeding this int -> NO rewrite *)

val lim_deriv = Unsynchronized.ref 100;

(* switch for checking guhs unique before storing a pbl or met;

   set true at startup (done at begin of ROOT.ML)

   set false for editing IsacKnowledge (done at end of ROOT.ML) *)

val check_guhs_unique = Unsynchronized.ref true;

(*\------- to Trace from Celem --------/*)

(**)end(**)