# HG changeset patch
# User wenzelm
# Date 1386934305 -3600
# Node ID b91afc3aa3e6d58e3fee6847a44b5a8c26b60edb
# Parent  92fa590bdfe0ead99b6f8c43f21f9977e737799c
clarified Proof General legacy: special treatment of \<^newline> only in TTY mode;

diff -r 92fa590bdfe0 -r b91afc3aa3e6 src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Thu Dec 12 23:18:47 2013 +0100
+++ b/src/Pure/General/symbol.ML	Fri Dec 13 12:31:45 2013 +0100
@@ -424,8 +424,7 @@
 
 val scan_encoded_newline =
   $$ "\^M" -- $$ "\n" >> K "\n" ||
-  $$ "\^M" >> K "\n" ||
-  Scan.this_string "\\<^newline>" >> K "\n";  (*Proof General legacy*)
+  $$ "\^M" >> K "\n";
 
 val scan_raw =
   Scan.this_string "raw:" ^^ (Scan.many raw_chr >> implode) ||
diff -r 92fa590bdfe0 -r b91afc3aa3e6 src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Thu Dec 12 23:18:47 2013 +0100
+++ b/src/Pure/General/symbol.scala	Fri Dec 13 12:31:45 2013 +0100
@@ -51,7 +51,7 @@
       case _ => !s.endsWith(">") || s == "\\<>" || s == "\\<^>"
     }
 
-  def is_physical_newline(s: Symbol): Boolean =
+  def is_newline(s: Symbol): Boolean =
     s == "\n" || s == "\r" || s == "\r\n"
 
   class Matcher(text: CharSequence)
@@ -102,7 +102,7 @@
   {
     var (line, column) = pos
     for (sym <- iterator(text)) {
-      if (is_physical_newline(sym)) { line += 1; column = 1 }
+      if (is_newline(sym)) { line += 1; column = 1 }
       else column += 1
     }
     (line, column)
@@ -358,7 +358,7 @@
       "\\<Xi>", "\\<Pi>", "\\<Sigma>", "\\<Upsilon>", "\\<Phi>",
       "\\<Psi>", "\\<Omega>")
 
-    val blanks = recode_set(" ", "\t", "\n", "\u000B", "\f", "\r", "\r\n", "\\<^newline>")
+    val blanks = recode_set(" ", "\t", "\n", "\u000B", "\f", "\r", "\r\n")
 
     val sym_chars =
       Set("!", "#", "$", "%", "&", "*", "+", "-", "/", "<", "=", ">", "?", "@", "^", "_", "|", "~")
diff -r 92fa590bdfe0 -r b91afc3aa3e6 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Thu Dec 12 23:18:47 2013 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Fri Dec 13 12:31:45 2013 +0100
@@ -267,13 +267,15 @@
 type isar =
   (Toplevel.transition, (Toplevel.transition option,
     (Token.T, (Token.T option, (Token.T, (Token.T,
-      (Symbol_Pos.T, Position.T * (Symbol.symbol, (string, unit) Source.source)
+      (Symbol_Pos.T,
+        Position.T * (Symbol.symbol, (Symbol.symbol, (string, unit) Source.source) Source.source)
   Source.source) Source.source) Source.source) Source.source)
   Source.source) Source.source) Source.source) Source.source;
 
 fun isar in_stream term : isar =
   Source.tty in_stream
   |> Symbol.source
+  |> Source.map_filter (fn "\\<^newline>" => SOME "\n" | s => SOME s)  (*Proof General legacy*)
   |> Token.source {do_recover = SOME true} Keyword.get_lexicons Position.none
   |> toplevel_source term (SOME true) lookup_commands_dynamic;