# 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 @@ "\\", "\\", "\\", "\\", "\\", "\\", "\\") - 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;