# HG changeset patch
# User wenzelm
# Date 1202672987 -3600
# Node ID f8ee5cbb3068f919bcdd2643c3f35f6575d40b9a
# Parent  7d5b3e34a7359bd52fe56f17d3076e9c8a2cfac5
tuned default position;

diff -r 7d5b3e34a735 -r f8ee5cbb3068 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Sun Feb 10 20:49:46 2008 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Sun Feb 10 20:49:47 2008 +0100
@@ -392,7 +392,7 @@
 (* nested commands *)
 
 fun nested_command props (str, pos) =
-  let val pos' = Position.of_properties (props @ Position.properties_of pos) in
+  let val pos' = Position.of_properties (props |> Position.default_properties pos) in
     (case OuterSyntax.parse pos' str of
       [transition] => transition
     | _ => error "exactly one command expected")
diff -r 7d5b3e34a735 -r f8ee5cbb3068 src/Pure/Tools/isabelle_process.ML
--- a/src/Pure/Tools/isabelle_process.ML	Sun Feb 10 20:49:46 2008 +0100
+++ b/src/Pure/Tools/isabelle_process.ML	Sun Feb 10 20:49:47 2008 +0100
@@ -96,9 +96,8 @@
       | SOME xml => (XML.plain_content xml, the_default Position.none (get_pos xml)))
       |>> translate_string (fn c => if c = STX then DEL else c);
     val props =
-      (case Position.properties_of (Position.thread_data ()) of
-        [] => Position.properties_of pos
-      | props => props);
+      Position.properties_of (Position.thread_data ())
+      |> Position.default_properties pos;
   in Output.writeln_default (special ch ^ print_props props ^ txt ^ special_end) end;
 
 fun init_message () =