Support for copy-avoiding functions on pure values, at the cost of readability.

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/same.ML	Thu Jul 16 16:24:49 2009 +0200
@@ -0,0 +1,36 @@
+(*  Title:      Pure/General/same.ML
+    Author:     Makarius
+
+Support for copy-avoiding functions on pure values, at the cost of
+readability.
+*)
+
+signature SAME =
+sig
+  exception SAME
+  type ('a, 'b) function = 'a -> 'b  (*exception SAME*)
+  type 'a operation = ('a, 'a) function  (*exception SAME*)
+  val commit: 'a operation -> 'a -> 'a
+  val function: ('a -> 'b option) -> ('a, 'b) function
+  val capture: ('a, 'b) function -> 'a -> 'b option
+end;
+
+structure Same: SAME =
+struct
+
+exception SAME;
+
+type ('a, 'b) function = 'a -> 'b;
+type 'a operation = ('a, 'a) function;
+
+fun commit f x = f x handle SAME => x;
+
+fun capture f x = SOME (f x) handle SAME => NONE;
+
+fun function f x =
+  (case f x of
+    NONE => raise SAME
+  | SOME y => y);
+
+
+end;

--- a/src/Pure/IsaMakefile	Thu Jul 16 00:24:11 2009 +0200
+++ b/src/Pure/IsaMakefile	Thu Jul 16 16:24:49 2009 +0200
@@ -52,12 +52,12 @@
   General/long_name.ML General/markup.ML General/name_space.ML		\
   General/ord_list.ML General/output.ML General/path.ML			\
   General/position.ML General/pretty.ML General/print_mode.ML		\
-  General/properties.ML General/queue.ML General/scan.ML		\
-  General/secure.ML General/seq.ML General/source.ML General/stack.ML	\
-  General/symbol.ML General/symbol_pos.ML General/table.ML		\
-  General/url.ML General/xml.ML General/yxml.ML Isar/args.ML		\
-  Isar/attrib.ML Isar/auto_bind.ML Isar/calculation.ML Isar/class.ML	\
-  Isar/class_target.ML Isar/code.ML Isar/constdefs.ML			\
+  General/properties.ML General/queue.ML General/same.ML		\
+  General/scan.ML General/secure.ML General/seq.ML General/source.ML	\
+  General/stack.ML General/symbol.ML General/symbol_pos.ML		\
+  General/table.ML General/url.ML General/xml.ML General/yxml.ML	\
+  Isar/args.ML Isar/attrib.ML Isar/auto_bind.ML Isar/calculation.ML	\
+  Isar/class.ML Isar/class_target.ML Isar/code.ML Isar/constdefs.ML	\
   Isar/context_rules.ML Isar/element.ML Isar/expression.ML		\
   Isar/isar_cmd.ML Isar/isar_document.ML Isar/isar_syn.ML		\
   Isar/local_defs.ML Isar/local_syntax.ML Isar/local_theory.ML		\

--- a/src/Pure/ROOT.ML	Thu Jul 16 00:24:11 2009 +0200
+++ b/src/Pure/ROOT.ML	Thu Jul 16 16:24:49 2009 +0200
@@ -33,11 +33,12 @@
 use "ML/ml_lex.ML";
 use "ML/ml_parse.ML";
 use "General/secure.ML";
-(*----- basic ML bootstrap finished -----*)
+(*^^^^^ end of basic ML bootstrap ^^^^^*)
 use "General/integer.ML";
 use "General/stack.ML";
 use "General/queue.ML";
 use "General/heap.ML";
+use "General/same.ML";
 use "General/ord_list.ML";
 use "General/balanced_tree.ML";
 use "General/graph.ML";