# HG changeset patch # User wenzelm # Date 1184879928 -7200 # Node ID 8f3099589cfabc4f3dfadc867934ec32945a0650 # Parent b1861768d8f45fceddea2cdd741d154e494d8723 tuned signature; diff -r b1861768d8f4 -r 8f3099589cfa src/Pure/General/path.ML --- a/src/Pure/General/path.ML Thu Jul 19 23:18:46 2007 +0200 +++ b/src/Pure/General/path.ML Thu Jul 19 23:18:48 2007 +0200 @@ -2,14 +2,12 @@ ID: $Id$ Author: Markus Wenzel, TU Muenchen -Abstract algebra of file paths (external encoding Unix-style). +Abstract algebra of file paths (external encoding in Unix style). *) signature PATH = sig - datatype elem = Root | Parent | Basic of string | Variable of string eqtype T - val rep: T -> elem list val is_current: T -> bool val current: T val root: T diff -r b1861768d8f4 -r 8f3099589cfa src/Pure/Thy/thy_header.ML --- a/src/Pure/Thy/thy_header.ML Thu Jul 19 23:18:46 2007 +0200 +++ b/src/Pure/Thy/thy_header.ML Thu Jul 19 23:18:48 2007 +0200 @@ -9,8 +9,7 @@ sig val args: OuterLex.token list -> (string * string list * (string * bool) list) * OuterLex.token list - val read: (string, 'a) Source.source * Position.T -> - string * string list * (string * bool) list + val read: Position.T -> (string, 'a) Source.source -> string * string list * (string * bool) list end; structure ThyHeader: THY_HEADER = @@ -49,7 +48,7 @@ (P.$$$ theoryN -- P.tags) |-- args)) || (P.$$$ theoryN -- P.tags) |-- P.!!! args; -fun read (src, pos) = +fun read pos src = let val res = src |> Symbol.source false diff -r b1861768d8f4 -r 8f3099589cfa src/Pure/Thy/thy_output.ML --- a/src/Pure/Thy/thy_output.ML Thu Jul 19 23:18:46 2007 +0200 +++ b/src/Pure/Thy/thy_output.ML Thu Jul 19 23:18:48 2007 +0200 @@ -21,7 +21,7 @@ datatype markup = Markup | MarkupEnv | Verbatim val modes: string list ref val eval_antiquote: Scan.lexicon -> Toplevel.node option -> string * Position.T -> string - val present_thy: Scan.lexicon -> (string -> string list) -> (markup -> string -> bool) -> + val process_thy: Scan.lexicon -> (string -> string list) -> (markup -> string -> bool) -> Toplevel.transition list -> (OuterLex.token, 'a) Source.source -> Buffer.T val output_list: (Proof.context -> 'a -> Pretty.T) -> Args.src -> Proof.context -> 'a list -> string @@ -286,7 +286,7 @@ end; -(* present_thy *) +(* process_thy *) datatype markup = Markup | MarkupEnv | Verbatim; @@ -317,7 +317,7 @@ in -fun present_thy lex default_tags is_markup trs src = +fun process_thy lex default_tags is_markup trs src = let (* tokens *)