tuned signature;
authorwenzelm
Thu Jul 19 23:18:48 2007 +0200 (2007-07-19)
changeset 238638f3099589cfa
parent 23862 b1861768d8f4
child 23864 365682a666da
tuned signature;
src/Pure/General/path.ML
src/Pure/Thy/thy_header.ML
src/Pure/Thy/thy_output.ML
     1.1 --- a/src/Pure/General/path.ML	Thu Jul 19 23:18:46 2007 +0200
     1.2 +++ b/src/Pure/General/path.ML	Thu Jul 19 23:18:48 2007 +0200
     1.3 @@ -2,14 +2,12 @@
     1.4      ID:         $Id$
     1.5      Author:     Markus Wenzel, TU Muenchen
     1.6  
     1.7 -Abstract algebra of file paths (external encoding Unix-style).
     1.8 +Abstract algebra of file paths (external encoding in Unix style).
     1.9  *)
    1.10  
    1.11  signature PATH =
    1.12  sig
    1.13 -  datatype elem = Root | Parent | Basic of string | Variable of string
    1.14    eqtype T
    1.15 -  val rep: T -> elem list
    1.16    val is_current: T -> bool
    1.17    val current: T
    1.18    val root: T
     2.1 --- a/src/Pure/Thy/thy_header.ML	Thu Jul 19 23:18:46 2007 +0200
     2.2 +++ b/src/Pure/Thy/thy_header.ML	Thu Jul 19 23:18:48 2007 +0200
     2.3 @@ -9,8 +9,7 @@
     2.4  sig
     2.5    val args: OuterLex.token list ->
     2.6      (string * string list * (string * bool) list) * OuterLex.token list
     2.7 -  val read: (string, 'a) Source.source * Position.T ->
     2.8 -    string * string list * (string * bool) list
     2.9 +  val read: Position.T -> (string, 'a) Source.source -> string * string list * (string * bool) list
    2.10  end;
    2.11  
    2.12  structure ThyHeader: THY_HEADER =
    2.13 @@ -49,7 +48,7 @@
    2.14      (P.$$$ theoryN -- P.tags) |-- args)) ||
    2.15    (P.$$$ theoryN -- P.tags) |-- P.!!! args;
    2.16  
    2.17 -fun read (src, pos) =
    2.18 +fun read pos src =
    2.19    let val res =
    2.20      src
    2.21      |> Symbol.source false
     3.1 --- a/src/Pure/Thy/thy_output.ML	Thu Jul 19 23:18:46 2007 +0200
     3.2 +++ b/src/Pure/Thy/thy_output.ML	Thu Jul 19 23:18:48 2007 +0200
     3.3 @@ -21,7 +21,7 @@
     3.4    datatype markup = Markup | MarkupEnv | Verbatim
     3.5    val modes: string list ref
     3.6    val eval_antiquote: Scan.lexicon -> Toplevel.node option -> string * Position.T -> string
     3.7 -  val present_thy: Scan.lexicon -> (string -> string list) -> (markup -> string -> bool) ->
     3.8 +  val process_thy: Scan.lexicon -> (string -> string list) -> (markup -> string -> bool) ->
     3.9      Toplevel.transition list -> (OuterLex.token, 'a) Source.source -> Buffer.T
    3.10    val output_list: (Proof.context -> 'a -> Pretty.T) -> Args.src ->
    3.11      Proof.context -> 'a list -> string
    3.12 @@ -286,7 +286,7 @@
    3.13  end;
    3.14  
    3.15  
    3.16 -(* present_thy *)
    3.17 +(* process_thy *)
    3.18  
    3.19  datatype markup = Markup | MarkupEnv | Verbatim;
    3.20  
    3.21 @@ -317,7 +317,7 @@
    3.22  
    3.23  in
    3.24  
    3.25 -fun present_thy lex default_tags is_markup trs src =
    3.26 +fun process_thy lex default_tags is_markup trs src =
    3.27    let
    3.28      (* tokens *)
    3.29