# HG changeset patch
# User wenzelm
# Date 1359115774 -3600
# Node ID 123be08eed88654bb032e1c334f40c7f281f728a
# Parent  2ad5c46bcd04f95d450faea07b5b8d3a44c16680
clarified notion of Command.proper_range (according to Token.is_proper), especially relevant for Active.try_replace_command, to avoid loosing subsequent comments accidentally;
reverted f3588e59aeaa accordingly;

diff -r 2ad5c46bcd04 -r 123be08eed88 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Thu Jan 24 21:18:30 2013 +0100
+++ b/src/Pure/Isar/proof.ML	Fri Jan 25 13:09:34 2013 +0100
@@ -1031,8 +1031,8 @@
 local
 
 fun skipped_proof state =
-  Context_Position.report_text (context_of state) (Position.thread_data ())
-    Markup.bad "Skipped proof";
+  Context_Position.if_visible (context_of state) Output.report
+    (Markup.markup Markup.bad "Skipped proof");
 
 in
 
diff -r 2ad5c46bcd04 -r 123be08eed88 src/Pure/Isar/token.scala
--- a/src/Pure/Isar/token.scala	Thu Jan 24 21:18:30 2013 +0100
+++ b/src/Pure/Isar/token.scala	Fri Jan 25 13:09:34 2013 +0100
@@ -89,6 +89,7 @@
   def is_text: Boolean = is_xname || kind == Token.Kind.VERBATIM
   def is_space: Boolean = kind == Token.Kind.SPACE
   def is_comment: Boolean = kind == Token.Kind.COMMENT
+  def is_improper: Boolean = is_space || is_comment
   def is_proper: Boolean = !is_space && !is_comment
   def is_error: Boolean = kind == Token.Kind.ERROR
   def is_unparsed: Boolean = kind == Token.Kind.UNPARSED
diff -r 2ad5c46bcd04 -r 123be08eed88 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Thu Jan 24 21:18:30 2013 +0100
+++ b/src/Pure/PIDE/command.scala	Fri Jan 25 13:09:34 2013 +0100
@@ -209,7 +209,7 @@
   val range: Text.Range = Text.Range(0, length)
 
   val proper_range: Text.Range =
-    Text.Range(0, (length /: span.reverse.iterator.takeWhile(_.is_space))(_ - _.source.length))
+    Text.Range(0, (length /: span.reverse.iterator.takeWhile(_.is_improper))(_ - _.source.length))
 
   def source(range: Text.Range): String = source.substring(range.start, range.stop)