# HG changeset patch
# User wenzelm
# Date 1380031572 -7200
# Node ID 88c6e630c15fc35c0a28ebcd557a0ba32a65909f
# Parent  b98c6cd902305bf34707085a3a8419b8cf642785
clarified command spans (again, see also 03a2dc9e0624): restrict to proper range to allow Isabelle.command_edit adding material monotonically without destroying the command (e.g. relevant for sendback from sledgehammer);
simplified command padding: always newline, despite lack of indentation;

diff -r b98c6cd90230 -r 88c6e630c15f src/Pure/Thy/thy_syntax.ML
--- a/src/Pure/Thy/thy_syntax.ML	Tue Sep 24 16:03:00 2013 +0200
+++ b/src/Pure/Thy/thy_syntax.ML	Tue Sep 24 16:06:12 2013 +0200
@@ -123,14 +123,21 @@
   else if forall Token.is_improper toks then Span (Ignored, toks)
   else Span (Malformed, toks);
 
-fun flush (result, span) = if null span then (result, span) else (rev span :: result, []);
+fun flush (result, span, improper) =
+  result
+  |> not (null span) ? cons (rev span)
+  |> not (null improper) ? cons (rev improper);
+
+fun parse tok (result, span, improper) =
+  if Token.is_command tok then (flush (result, span, improper), [tok], [])
+  else if Token.is_improper tok then (result, span, tok :: improper)
+  else (result, tok :: (improper @ span), []);
 
 in
 
 fun parse_spans toks =
-  fold (fn tok => Token.is_command tok ? flush #> apsnd (cons tok)) toks ([], [])
-  |> flush
-  |> #1 |> rev |> map make_span;
+  fold parse toks ([], [], [])
+  |> flush |> rev |> map make_span;
 
 end;
 
diff -r b98c6cd90230 -r 88c6e630c15f src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Tue Sep 24 16:03:00 2013 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Tue Sep 24 16:06:12 2013 +0200
@@ -81,10 +81,20 @@
   {
     val result = new mutable.ListBuffer[List[Token]]
     val span = new mutable.ListBuffer[Token]
+    val improper = new mutable.ListBuffer[Token]
 
-    def flush() { if (!span.isEmpty) { result += span.toList; span.clear } }
-    for (tok <- toks) { if (tok.is_command) flush(); span += tok }
+    def flush()
+    {
+      if (!span.isEmpty) { result += span.toList; span.clear }
+      if (!improper.isEmpty) { result += improper.toList; improper.clear }
+    }
+    for (tok <- toks) {
+      if (tok.is_command) { flush(); span += tok }
+      else if (tok.is_improper) improper += tok
+      else { span ++= improper; improper.clear; span += tok }
+    }
     flush()
+
     result.toList
   }
 
diff -r b98c6cd90230 -r 88c6e630c15f src/Tools/jEdit/src/isabelle.scala
--- a/src/Tools/jEdit/src/isabelle.scala	Tue Sep 24 16:03:00 2013 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala	Tue Sep 24 16:06:12 2013 +0200
@@ -187,13 +187,7 @@
             JEdit_Lib.buffer_edit(buffer) {
               val range = command.proper_range + start
               if (padding) {
-                val pad =
-                  JEdit_Lib.try_get_text(buffer, Text.Range(range.length - 1, range.length))
-                    match {
-                      case None => ""
-                      case Some(s) => if (Symbol.is_blank(s)) "" else " "
-                    }
-                buffer.insert(start + range.length, pad + s)
+                buffer.insert(start + range.length, "\n" + s)
               }
               else {
                 buffer.remove(start, range.length)