# HG changeset patch
# User wenzelm
# Date 1357998437 -3600
# Node ID 777c6026ca934578ed41b1ef5ee08e6c9fbb7ffa
# Parent  9cc70b273e90babce50aa18ad180c33854e5915c
tuned signature;

diff -r 9cc70b273e90 -r 777c6026ca93 src/Pure/General/properties.ML
--- a/src/Pure/General/properties.ML	Fri Jan 11 22:38:12 2013 +0100
+++ b/src/Pure/General/properties.ML	Sat Jan 12 14:47:17 2013 +0100
@@ -6,17 +6,19 @@
 
 signature PROPERTIES =
 sig
-  type T = (string * string) list
+  type entry = string * string
+  type T = entry list
   val defined: T -> string -> bool
   val get: T -> string -> string option
-  val put: string * string -> T -> T
+  val put: entry -> T -> T
   val remove: string -> T -> T
 end;
 
 structure Properties: PROPERTIES =
 struct
 
-type T = (string * string) list;
+type entry = string * string;
+type T = entry list;
 
 fun defined (props: T) name = AList.defined (op =) props name;
 fun get (props: T) name = AList.lookup (op =) props name;
diff -r 9cc70b273e90 -r 777c6026ca93 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Fri Jan 11 22:38:12 2013 +0100
+++ b/src/Pure/PIDE/markup.ML	Sat Jan 12 14:47:17 2013 +0100
@@ -125,14 +125,14 @@
   val graphviewN: string
   val sendbackN: string
   val paddingN: string
-  val padding_line: string * string
+  val padding_line: Properties.entry
   val dialogN: string val dialog: serial -> string -> T
   val functionN: string
   val assign_execs: Properties.T
   val removed_versions: Properties.T
   val invoke_scala: string -> string -> Properties.T
   val cancel_scala: string -> Properties.T
-  val ML_statistics: string * string
+  val ML_statistics: Properties.entry
   val no_output: Output.output * Output.output
   val default_output: T -> Output.output * Output.output
   val add_mode: string -> (T -> Output.output * Output.output) -> unit