--- a/ProgTutorial/Base.thy	Fri Oct 02 15:38:14 2009 +0200
+++ b/ProgTutorial/Base.thy	Sat Oct 03 13:01:39 2009 +0200
@@ -17,7 +17,7 @@
 
 ML {*
 (* FIXME ref *)
-val file_name = ref (NONE : string option)
+val file_name = Unsynchronized.ref (NONE : string option)
 
 fun write_file txt =
   case !file_name of

--- a/ProgTutorial/FirstSteps.thy	Fri Oct 02 15:38:14 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy	Sat Oct 03 13:01:39 2009 +0200
@@ -57,7 +57,7 @@
 *}
 
 ML %gray {* 
-  val r = ref 0
+  val r = Unsynchronized.ref 0
   fun f n = n + 1 
 *}
 
@@ -274,7 +274,7 @@
   @{text "?Q"} and so on. They are needed in order to able to
   instantiate theorems when they are applied. For example the theorem 
   @{thm [source] conjI} shown below can be used for any (typable) 
-  instantiation of @{text "?P"} and @{text "?Q"} 
+  instantiation of @{text "?P"} and @{text "?Q"}. 
 
   @{ML_response_fake [display, gray]
   "tracing (string_of_thm @{context} @{thm conjI})"
@@ -844,7 +844,7 @@
   \end{readmore}
 *}
 
-section {* Storing Data in Isabelle *}
+section {* Storing Data in Isabelle\label{sec:storing} *}
 
 text {*
   Isabelle provides mechanisms for storing (and retrieving) arbitrary
@@ -914,18 +914,20 @@
   This runtime error is the reason why ML is still type-sound despite
   containing a universal type.
 
-  Now, Isabelle heavily uses this mechanism to store all sorts of data: theorem lists,
-  simpsets, facts etc.  Roughly speaking, there are two places where data can 
-  be stored: in \emph{theories} and in \emph{proof contexts}. Again
-  roughly speaking, data such as simpsets need to be stored in a theory,
-  since they need to be maintained across proofs and even theories.
-  On the other hands, data such as facts change inside a proof and
-  therefore need to be maintained inside a proof 
-  context.\footnote{\bf TODO: explain more bout this.} 
+  Now, Isabelle heavily uses this mechanism for storing all sorts of
+  data: theorem lists, simpsets, facts etc.  Roughly speaking, there are two
+  places where data can be stored: in \emph{theories} and in \emph{proof
+  contexts}. Again roughly speaking, data such as simpsets need to be stored
+  in a theory, since they need to be maintained across proofs and even across
+  theories.  On the other hand, data such as facts change inside a proof and
+  are only relevant to the proof at hand. Therefore such data needs to be 
+  maintained inside a proof context.\footnote{\bf TODO: explain more about 
+  this in a separate section.}
 
-  For both theories and proof contexts there are convenient functors that help
+  For theories and proof contexts there are, respectively, the functors 
+  @{ML_funct_ind TheoryDataFun} and @{ML_funct_ind ProofDataFun} that help
   with the data storage. Below we show how to implement a table in which we
-  can store theorems that can be looked up according to a string key. The
+  can store theorems and look them up according to a string key. The
   intention is to be able to look up introduction rules for logical
   connectives. Such a table might be useful in an automatic proof procedure
   and therefore it makes sense to store this data inside a theory.  The code
@@ -949,9 +951,9 @@
   roughly to the operations performed on theories.\footnote{\bf FIXME: Say more
   about the assumptions of these operations.} The result structure @{ML_text Data}
   contains functions for accessing the table (@{ML Data.get}) and for updating
-  it (@{ML Data.map}). There are also two more functions, which however we
-  ignore here. Below we define two auxiliary functions, which help us with
-  accessing the table.
+  it (@{ML Data.map}). There are also two more functions (@{ML Data.init} and 
+  @{ML Data.put}), which however we ignore here. Below we define two auxiliary 
+  functions, which help us with accessing the table.
 *}
 
 ML{*val lookup = Symtab.lookup o Data.get
@@ -969,8 +971,9 @@
 *}
 
 text {*
-  The use of \isacommand{setup} makes sure the table in the current theory 
-  is updated. The lookup can now be performed as follows.
+  The use of the command \isacommand{setup} makes sure the table in the 
+  \emph{current} theory is updated. The lookup can now be performed as 
+  follows.
 
   @{ML_response_fake [display, gray]
 "lookup @{theory} \"op &\""
@@ -984,78 +987,87 @@
 setup %gray {* update "op &" @{thm TrueI} *}
 
 text {*
-  and lookup now produces the introduction rule for @{term "True"}
+  and @{ML lookup} now produces the introduction rule for @{term "True"}
   
 @{ML_response_fake [display, gray]
 "lookup @{theory} \"op &\""
 "SOME \"True\""}
 
   there are no references involved. This is one of the most fundamental
-  coding conventions for programming in Isabelle. References would interfere
-  with the multithreaded execution model of Isabelle.\footnote{\bf FIXME: say more}
-  
-  \begin{readmore}
-  Isabelle contains implementations of several container data structures,
-  including association lists in @{ML_file "Pure/General/alist.ML"},
-  tables and symtables in @{ML_file "Pure/General/table.ML"}, and
-  directed graphs in @{ML_file "Pure/General/graph.ML"}.
-  \end{readmore}
-
-  Storing data in a proof context is similar. With the following code we
-  can store a list of terms in a proof context. 
+  coding conventions for programming in Isabelle. References would 
+  interfere with the multithreaded execution model of Isabelle and also
+  defeat the undo-mechanism in proof scripts. For this consider the 
+  following data container where we maintain a reference to a list of 
+  integers.
 *}
 
-ML{*structure Data = ProofDataFun
-  (type T = term list
-   val init = (K []))*}
+ML{*structure WrongRefData = TheoryDataFun
+  (type T = (int list) Unsynchronized.ref
+   val empty = Unsynchronized.ref []
+   val copy = I
+   val extend = I
+   fun merge _ = fst)*}
 
 text {*
-  The function we have to specify has to produce a list once a context 
-  is initialised (taking the theory into account from which the 
-  context is derived). We choose to just return the empty list. Next 
-  we define two auxiliary functions for updating the list with a given
-  term and printing the list. 
+  We initialise the reference with the empty list. Consequently a first 
+  lookup produces @{ML "ref []" in Unsynchronized}.
+
+  @{ML_response_fake [display,gray]
+  "WrongRefData.get @{theory}"
+  "ref []"}
+
+  For updating the reference we use the following function.
+*}
+
+ML{*fun ref_update n = WrongRefData.map 
+      (fn r => let val _ = r := n::(!r) in r end)*}
+
+text {*
+  As above we update the reference with the command 
+  \isacommand{setup}. 
 *}
 
-ML{*fun update trm = Data.map (fn xs => trm::xs)
-
-fun print ctxt =
-  case (Data.get ctxt) of
-    [] => tracing "Empty!"
-  | xs => tracing (string_of_terms ctxt xs)*}
+setup %gray{* ref_update 1 *}
 
 text {*
-  Next we start with the context given by @{text "@{context}"} and 
-  update it in various ways. 
+  A lookup in the current theory gives then the expected list 
+  @{ML "ref [1]" in Unsynchronized}.
+
+  @{ML_response_fake [display,gray]
+  "WrongRefData.get @{theory}"
+  "ref [1]"}
+
+  So far everything is as expected. But, the trouble starts if we attempt
+  to backtrack to ``before'' the \isacommand{setup}-command. There, we 
+  would expect that the list is empty again. But since it is stored in 
+  a reference, Isabelle has no control over it. So it is not
+  empty, but still @{ML "ref [1]" in Unsynchronized}. Adding to the trouble, 
+  if we execute the \isacommand{setup}-command again, we do not obtain 
+  @{ML "ref [1]" in Unsynchronized}, but
 
   @{ML_response_fake [display,gray]
-"let
-  val ctxt    = @{context}
-  val ctxt'   = ctxt   |> update @{term \"False\"}
-                       |> update @{term \"True \<and> True\"} 
-  val ctxt''  = ctxt   |> update @{term \"1::nat\"}
-  val ctxt''' = ctxt'' |> update @{term \"2::nat\"}
-in
-  print ctxt; 
-  print ctxt';
-  print ctxt'';
-  print ctxt'''
-end"
-"Empty!
-True \<and> True, False
-1
-2, 1"}
+  "WrongRefData.get @{theory}"
+  "ref [1, 1]"}
+
+  Now imagine how often you go backwards and forwards in your proof scripts. 
+  By using references in Isabelle code, you are bound to cause all
+  hell to break lose. Therefore observe the coding convention: 
+  Do not use references for storing data!
 
-  Many functions in Isabelle manage and update data in a similar
-  fashion. Consequently, such calculation with contexts occur frequently in
-  Isabelle code, although the ``context flow'' is usually only linear.
+  \begin{readmore}
+  The functors for data storage are defined in @{ML_file "Pure/context.ML"}.
+  Isabelle contains implementations of several container data structures,
+  including association lists in @{ML_file "Pure/General/alist.ML"},
+  directed graphs in @{ML_file "Pure/General/graph.ML"}. and 
+  tables and symtables in @{ML_file "Pure/General/table.ML"}.
+  \end{readmore}
 
-  A special instance of the mechanisms described above are configuration
-  values. They are used to in order to configure tools by the user without
-  having to resort to the ML-level. Assume you want the user to control three
-  values, say @{text bval} containing a boolean, @{text ival} containing an
-  integer and @{text sval} containing a string. These values can be declared
-  by
+  A special instance of the data storage mechanism described above are
+  configuration values. They are used to enable users to configure tools
+  without having to resort to the ML-level (and also to avoid
+  references). Assume you want the user to control three values, say @{text
+  bval} containing a boolean, @{text ival} containing an integer and @{text
+  sval} containing a string. These values can be declared by
 *}
 
 ML{*val (bval, setup_bval) = Attrib.config_bool "bval" false
@@ -1081,7 +1093,7 @@
 
 text {*
   On the ML-level these values can be retrieved using the 
-  function @{ML Config.get}:
+  function @{ML Config.get}.
 
   @{ML_response [display,gray] "Config.get @{context} bval" "true"}
 
@@ -1089,6 +1101,61 @@
   For more information about configuration values see 
   @{ML_file "Pure/Isar/attrib.ML"} and @{ML_file "Pure/config.ML"}.
   \end{readmore}
+
+  Storing data in a proof context is done in a similar fashion. The
+  corresponding functor is @{ML_funct_ind ProofDataFun}. With the 
+  following code we can store a list of terms in a proof context. 
+*}
+
+ML{*structure Data = ProofDataFun
+  (type T = term list
+   fun init _ = [])*}
+
+text {*
+  The function we have to specify has to produce a list once a context 
+  is initialised (taking the theory into account from which the 
+  context is derived). We choose to just return the empty list. Next 
+  we define two auxiliary functions for updating the list with a given
+  term and printing the list. 
+*}
+
+ML{*fun update trm = Data.map (fn xs => trm::xs)
+
+fun print ctxt =
+  case (Data.get ctxt) of
+    [] => tracing "Empty!"
+  | xs => tracing (string_of_terms ctxt xs)*}
+
+text {*
+  Next we start with the context given by the antiquotation 
+  @{text "@{context}"} and update it in various ways. 
+
+  @{ML_response_fake [display,gray]
+"let
+  val ctxt    = @{context}
+  val ctxt'   = ctxt   |> update @{term \"False\"}
+                       |> update @{term \"True \<and> True\"} 
+  val ctxt''  = ctxt   |> update @{term \"1::nat\"}
+  val ctxt''' = ctxt'' |> update @{term \"2::nat\"}
+in
+  print ctxt; 
+  print ctxt';
+  print ctxt'';
+  print ctxt'''
+end"
+"Empty!
+True \<and> True, False
+1
+2, 1"}
+
+  Many functions in Isabelle manage and update data in a similar
+  fashion. Consequently, such calculation with contexts occur frequently in
+  Isabelle code, although the ``context flow'' is usually only linear.
+  Note also that the calculation above has no effect on the underlying
+  theory. Once we throw away the contexts, we have no access to their
+  associated data. This is different to theories, where the command 
+  \isacommand{setup} registers the data with the current and future 
+  theories, and therefore can access the data potentially indefinitely. 
 *}
 
 

--- a/ProgTutorial/General.thy	Fri Oct 02 15:38:14 2009 +0200
+++ b/ProgTutorial/General.thy	Sat Oct 03 13:01:39 2009 +0200
@@ -1000,7 +1000,7 @@
   of theorems.
 *}
 
-ML{*val my_thms = ref ([] : thm list)*}
+ML{*val my_thms = Unsynchronized.ref ([] : thm list)*}
 
 text {* 
   The purpose of this reference is to store a list of theorems.

--- a/ProgTutorial/Helper/Command/Command.thy	Fri Oct 02 15:38:14 2009 +0200
+++ b/ProgTutorial/Helper/Command/Command.thy	Sat Oct 03 13:01:39 2009 +0200
@@ -40,7 +40,7 @@
 *}
 
 ML {*
-val r = ref (NONE:(unit -> term) option)
+val r = Unsynchronized.ref (NONE:(unit -> term) option)
 *}
 ML{*
 let

--- a/ProgTutorial/Intro.thy	Fri Oct 02 15:38:14 2009 +0200
+++ b/ProgTutorial/Intro.thy	Sat Oct 03 13:01:39 2009 +0200
@@ -207,8 +207,9 @@
   \item {\bf Jasmin Blanchette} helped greatly with section \ref{sec:pretty}.
 
   \item {\bf Sascha Böhme} contributed the recipes in \ref{rec:timeout}, 
-  \ref{rec:config}, \ref{rec:storingdata}, \ref{rec:external} and \ref{rec:oracle}.
-  He also wrote section \ref{sec:conversion} and helped with recipe \ref{rec:timing}.
+  \ref{rec:external} and \ref{rec:oracle}. He also wrote section \ref{sec:conversion} 
+  and helped with recipe \ref{rec:timing}. Parts of the section \ref{sec:storing}
+  are by him.
 
   \item {\bf Jeremy Dawson} wrote the first version of the chapter
   about parsing.

--- a/ProgTutorial/Parsing.thy	Fri Oct 02 15:38:14 2009 +0200
+++ b/ProgTutorial/Parsing.thy	Sat Oct 03 13:01:39 2009 +0200
@@ -1089,7 +1089,7 @@
   
 *}
 
-ML_val{*val r = ref (NONE:(unit -> term) option)*}
+ML_val{*val r = Unsynchronized.ref (NONE:(unit -> term) option)*}
 ML{*let
    fun after_qed thm_name thms lthy =
         LocalTheory.note Thm.theoremK (thm_name, (flat thms)) lthy |> snd

--- a/ProgTutorial/ROOT.ML	Fri Oct 02 15:38:14 2009 +0200
+++ b/ProgTutorial/ROOT.ML	Sat Oct 03 13:01:39 2009 +0200
@@ -1,4 +1,4 @@
-set quick_and_dirty;
+quick_and_dirty := true;
 
 no_document use_thy "Base";
 no_document use_thy "Package/Simple_Inductive_Package";

--- a/ProgTutorial/Solutions.thy	Fri Oct 02 15:38:14 2009 +0200
+++ b/ProgTutorial/Solutions.thy	Sat Oct 03 13:01:39 2009 +0200
@@ -273,7 +273,7 @@
 
 ML{*fun term_tree n =
 let
-  val count = ref 0; 
+  val count = Unsynchronized.ref 0; 
 
   fun term_tree_aux n =
     case n of

--- a/ProgTutorial/antiquote_setup.ML	Fri Oct 02 15:38:14 2009 +0200
+++ b/ProgTutorial/antiquote_setup.ML	Sat Oct 03 13:01:39 2009 +0200
@@ -63,6 +63,13 @@
 val output_struct = gen_output_struct (K output)
 val output_struct_ind = gen_output_struct output_indexed
 
+(* prints functors; no checks *)
+fun gen_output_funct outfn {context = ctxt, ...} txt = 
+  (outfn {main = Code txt, minor = Plain "functor"} (split_lines txt))
+
+val output_funct = gen_output_funct (K output)
+val output_funct_ind = gen_output_funct output_indexed
+
 (* checks and prints types *)
 fun gen_output_type outfn {context = ctxt, ...} txt = 
   (eval_fn ctxt (ml_type txt); 
@@ -95,6 +102,8 @@
 val _ = ThyOutput.antiquotation "ML_type_ind" single_arg output_type_ind
 val _ = ThyOutput.antiquotation "ML_struct" single_arg output_struct
 val _ = ThyOutput.antiquotation "ML_struct_ind" single_arg output_struct_ind
+val _ = ThyOutput.antiquotation "ML_funct" single_arg output_funct
+val _ = ThyOutput.antiquotation "ML_funct_ind" single_arg output_funct_ind
 val _ = ThyOutput.antiquotation "ML_response" two_args output_response
 val _ = ThyOutput.antiquotation "ML_response_fake" two_args output_response_fake
 val _ = ThyOutput.antiquotation "ML_response_fake_both" two_args ouput_response_fake_both

--- a/ProgTutorial/output_tutorial.ML	Fri Oct 02 15:38:14 2009 +0200
+++ b/ProgTutorial/output_tutorial.ML	Sat Oct 03 13:01:39 2009 +0200
@@ -5,8 +5,8 @@
 (* rebuilding the output function from ThyOutput in order to *)
 (* enable the options [gray, linenos]                        *)
 
-val gray = ref false
-val linenos = ref false
+val gray = Unsynchronized.ref false
+val linenos = Unsynchronized.ref false
 
 
 fun output txt =

Binary file progtutorial.pdf has changed