tuned signature;
authorwenzelm
Mon May 17 15:02:44 2010 +0200 (2010-05-17)
changeset 36957cdb9e83abfbe
parent 36956 21be4832c362
child 36958 ad5313f1bd30
tuned signature;
src/Pure/General/symbol_pos.ML
     1.1 --- a/src/Pure/General/symbol_pos.ML	Mon May 17 14:23:54 2010 +0200
     1.2 +++ b/src/Pure/General/symbol_pos.ML	Mon May 17 15:02:44 2010 +0200
     1.3 @@ -4,17 +4,12 @@
     1.4  Symbols with explicit position information.
     1.5  *)
     1.6  
     1.7 -signature BASIC_SYMBOL_POS =
     1.8 +signature SYMBOL_POS =
     1.9  sig
    1.10    type T = Symbol.symbol * Position.T
    1.11    val symbol: T -> Symbol.symbol
    1.12    val $$$ : Symbol.symbol -> T list -> T list * T list
    1.13    val ~$$$ : Symbol.symbol -> T list -> T list * T list
    1.14 -end
    1.15 -
    1.16 -signature SYMBOL_POS =
    1.17 -sig
    1.18 -  include BASIC_SYMBOL_POS
    1.19    val content: T list -> string
    1.20    val untabify_content: T list -> string
    1.21    val is_eof: T -> bool
    1.22 @@ -185,5 +180,10 @@
    1.23  
    1.24  end;
    1.25  
    1.26 -structure Basic_Symbol_Pos: BASIC_SYMBOL_POS = Symbol_Pos;   (*not open by default*)
    1.27 +structure Basic_Symbol_Pos =   (*not open by default*)
    1.28 +struct
    1.29 +  val symbol = Symbol_Pos.symbol;
    1.30 +  val $$$ = Symbol_Pos.$$$;
    1.31 +  val ~$$$ = Symbol_Pos.~$$$;
    1.32 +end;
    1.33