discontinued special treatment of hard tabulators;
authorwenzelm
Fri Jul 08 16:13:34 2011 +0200 (2011-07-08)
changeset 43709717e96cf9527
parent 43708 b6601923cf1f
child 43710 7270ae921cf2
discontinued special treatment of hard tabulators;
NEWS
src/Pure/General/symbol_pos.ML
src/Pure/Isar/token.ML
src/Pure/Thy/latex.ML
     1.1 --- a/NEWS	Fri Jul 08 16:01:14 2011 +0200
     1.2 +++ b/NEWS	Fri Jul 08 16:13:34 2011 +0200
     1.3 @@ -123,6 +123,9 @@
     1.4  
     1.5  *** Document preparation ***
     1.6  
     1.7 +* Discontinued special treatment of hard tabulators, which are better
     1.8 +avoided in the first place.  Implicit tab-width is 1.
     1.9 +
    1.10  * Antiquotation @{rail} layouts railroad syntax diagrams, see also
    1.11  isar-ref manual.
    1.12  
     2.1 --- a/src/Pure/General/symbol_pos.ML	Fri Jul 08 16:01:14 2011 +0200
     2.2 +++ b/src/Pure/General/symbol_pos.ML	Fri Jul 08 16:13:34 2011 +0200
     2.3 @@ -11,7 +11,6 @@
     2.4    val $$$ : Symbol.symbol -> T list -> T list * T list
     2.5    val ~$$$ : Symbol.symbol -> T list -> T list * T list
     2.6    val content: T list -> string
     2.7 -  val untabify_content: T list -> string
     2.8    val is_eof: T -> bool
     2.9    val stopper: T Scan.stopper
    2.10    val !!! : string -> (T list -> 'a) -> T list -> 'a
    2.11 @@ -42,23 +41,9 @@
    2.12  
    2.13  fun symbol ((s, _): T) = s;
    2.14  
    2.15 -
    2.16 -(* content *)
    2.17 -
    2.18  val content = implode o map symbol;
    2.19  
    2.20  
    2.21 -val tab_width = (8: int);
    2.22 -
    2.23 -fun untabify ("\t", pos) =
    2.24 -      (case Position.column_of pos of
    2.25 -        SOME n => Symbol.spaces (tab_width - ((n - 1) mod tab_width))
    2.26 -      | NONE => Symbol.space)
    2.27 -  | untabify (s, _) = s;
    2.28 -
    2.29 -val untabify_content = implode o map untabify;
    2.30 -
    2.31 -
    2.32  (* stopper *)
    2.33  
    2.34  fun mk_eof pos = (Symbol.eof, pos);
     3.1 --- a/src/Pure/Isar/token.ML	Fri Jul 08 16:01:14 2011 +0200
     3.2 +++ b/src/Pure/Isar/token.ML	Fri Jul 08 16:13:34 2011 +0200
     3.3 @@ -319,10 +319,10 @@
     3.4  fun token_leq ((_, syms1), (_, syms2)) = length syms1 <= length syms2;
     3.5  
     3.6  fun token k ss =
     3.7 -  Token ((Symbol_Pos.implode ss, Symbol_Pos.range ss), (k, Symbol_Pos.untabify_content ss), Slot);
     3.8 +  Token ((Symbol_Pos.implode ss, Symbol_Pos.range ss), (k, Symbol_Pos.content ss), Slot);
     3.9  
    3.10  fun token_range k (pos1, (ss, pos2)) =
    3.11 -  Token (Symbol_Pos.implode_range pos1 pos2 ss, (k, Symbol_Pos.untabify_content ss), Slot);
    3.12 +  Token (Symbol_Pos.implode_range pos1 pos2 ss, (k, Symbol_Pos.content ss), Slot);
    3.13  
    3.14  fun scan (lex1, lex2) = !!! "bad input"
    3.15    (Symbol_Pos.scan_string_qq >> token_range String ||
     4.1 --- a/src/Pure/Thy/latex.ML	Fri Jul 08 16:01:14 2011 +0200
     4.2 +++ b/src/Pure/Thy/latex.ML	Fri Jul 08 16:13:34 2011 +0200
     4.3 @@ -83,6 +83,7 @@
     4.4      ("~", "{\\isachartilde}")];
     4.5  
     4.6  fun output_chr " " = "\\ "
     4.7 +  | output_chr "\t" = "\\ "
     4.8    | output_chr "\n" = "\\isanewline\n"
     4.9    | output_chr c =
    4.10        (case Symtab.lookup char_table c of