# HG changeset patch
# User wenzelm
# Date 1310134414 -7200
# Node ID 717e96cf9527e3d926cef22398cfd23f66968f2a
# Parent  b6601923cf1f3270120cf26a92f6cd5ce8cf00f7
discontinued special treatment of hard tabulators;

diff -r b6601923cf1f -r 717e96cf9527 NEWS
--- a/NEWS	Fri Jul 08 16:01:14 2011 +0200
+++ b/NEWS	Fri Jul 08 16:13:34 2011 +0200
@@ -123,6 +123,9 @@
 
 *** Document preparation ***
 
+* Discontinued special treatment of hard tabulators, which are better
+avoided in the first place.  Implicit tab-width is 1.
+
 * Antiquotation @{rail} layouts railroad syntax diagrams, see also
 isar-ref manual.
 
diff -r b6601923cf1f -r 717e96cf9527 src/Pure/General/symbol_pos.ML
--- a/src/Pure/General/symbol_pos.ML	Fri Jul 08 16:01:14 2011 +0200
+++ b/src/Pure/General/symbol_pos.ML	Fri Jul 08 16:13:34 2011 +0200
@@ -11,7 +11,6 @@
   val $$$ : Symbol.symbol -> T list -> T list * T list
   val ~$$$ : Symbol.symbol -> T list -> T list * T list
   val content: T list -> string
-  val untabify_content: T list -> string
   val is_eof: T -> bool
   val stopper: T Scan.stopper
   val !!! : string -> (T list -> 'a) -> T list -> 'a
@@ -42,23 +41,9 @@
 
 fun symbol ((s, _): T) = s;
 
-
-(* content *)
-
 val content = implode o map symbol;
 
 
-val tab_width = (8: int);
-
-fun untabify ("\t", pos) =
-      (case Position.column_of pos of
-        SOME n => Symbol.spaces (tab_width - ((n - 1) mod tab_width))
-      | NONE => Symbol.space)
-  | untabify (s, _) = s;
-
-val untabify_content = implode o map untabify;
-
-
 (* stopper *)
 
 fun mk_eof pos = (Symbol.eof, pos);
diff -r b6601923cf1f -r 717e96cf9527 src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Fri Jul 08 16:01:14 2011 +0200
+++ b/src/Pure/Isar/token.ML	Fri Jul 08 16:13:34 2011 +0200
@@ -319,10 +319,10 @@
 fun token_leq ((_, syms1), (_, syms2)) = length syms1 <= length syms2;
 
 fun token k ss =
-  Token ((Symbol_Pos.implode ss, Symbol_Pos.range ss), (k, Symbol_Pos.untabify_content ss), Slot);
+  Token ((Symbol_Pos.implode ss, Symbol_Pos.range ss), (k, Symbol_Pos.content ss), Slot);
 
 fun token_range k (pos1, (ss, pos2)) =
-  Token (Symbol_Pos.implode_range pos1 pos2 ss, (k, Symbol_Pos.untabify_content ss), Slot);
+  Token (Symbol_Pos.implode_range pos1 pos2 ss, (k, Symbol_Pos.content ss), Slot);
 
 fun scan (lex1, lex2) = !!! "bad input"
   (Symbol_Pos.scan_string_qq >> token_range String ||
diff -r b6601923cf1f -r 717e96cf9527 src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Fri Jul 08 16:01:14 2011 +0200
+++ b/src/Pure/Thy/latex.ML	Fri Jul 08 16:13:34 2011 +0200
@@ -83,6 +83,7 @@
     ("~", "{\\isachartilde}")];
 
 fun output_chr " " = "\\ "
+  | output_chr "\t" = "\\ "
   | output_chr "\n" = "\\isanewline\n"
   | output_chr c =
       (case Symtab.lookup char_table c of