1.1 --- a/src/Pure/Isar/proof.ML	Thu Jan 24 21:18:30 2013 +0100
     1.2 +++ b/src/Pure/Isar/proof.ML	Fri Jan 25 13:09:34 2013 +0100
     1.3 @@ -1031,8 +1031,8 @@
     1.4  local
     1.5  
     1.6  fun skipped_proof state =
     1.7 -  Context_Position.report_text (context_of state) (Position.thread_data ())
     1.8 -    Markup.bad "Skipped proof";
     1.9 +  Context_Position.if_visible (context_of state) Output.report
    1.10 +    (Markup.markup Markup.bad "Skipped proof");
    1.11  
    1.12  in
    1.13  

     2.1 --- a/src/Pure/Isar/token.scala	Thu Jan 24 21:18:30 2013 +0100
     2.2 +++ b/src/Pure/Isar/token.scala	Fri Jan 25 13:09:34 2013 +0100
     2.3 @@ -89,6 +89,7 @@
     2.4    def is_text: Boolean = is_xname || kind == Token.Kind.VERBATIM
     2.5    def is_space: Boolean = kind == Token.Kind.SPACE
     2.6    def is_comment: Boolean = kind == Token.Kind.COMMENT
     2.7 +  def is_improper: Boolean = is_space || is_comment
     2.8    def is_proper: Boolean = !is_space && !is_comment
     2.9    def is_error: Boolean = kind == Token.Kind.ERROR
    2.10    def is_unparsed: Boolean = kind == Token.Kind.UNPARSED

     3.1 --- a/src/Pure/PIDE/command.scala	Thu Jan 24 21:18:30 2013 +0100
     3.2 +++ b/src/Pure/PIDE/command.scala	Fri Jan 25 13:09:34 2013 +0100
     3.3 @@ -209,7 +209,7 @@
     3.4    val range: Text.Range = Text.Range(0, length)
     3.5  
     3.6    val proper_range: Text.Range =
     3.7 -    Text.Range(0, (length /: span.reverse.iterator.takeWhile(_.is_space))(_ - _.source.length))
     3.8 +    Text.Range(0, (length /: span.reverse.iterator.takeWhile(_.is_improper))(_ - _.source.length))
     3.9  
    3.10    def source(range: Text.Range): String = source.substring(range.start, range.stop)
    3.11