Pure/Thy/thy_parse/THY_PARSE: deleted duplicate specifications of parens,
authorlcp
Mon Aug 22 11:07:40 1994 +0200 (1994-08-22)
changeset 5706333c181a3f7
parent 569 4dc184a3d09b
child 571 0b03ce5b62f7
Pure/Thy/thy_parse/THY_PARSE: deleted duplicate specifications of parens,
brackets, ..., mk_triple
src/Pure/Thy/thy_parse.ML
     1.1 --- a/src/Pure/Thy/thy_parse.ML	Mon Aug 22 11:03:52 1994 +0200
     1.2 +++ b/src/Pure/Thy/thy_parse.ML	Mon Aug 22 11:07:40 1994 +0200
     1.3 @@ -43,12 +43,6 @@
     1.4    val sort: token list -> string * token list
     1.5    val opt_infix: token list -> string * token list
     1.6    val opt_mixfix: token list -> string * token list
     1.7 -  val parens: string -> string
     1.8 -  val brackets: string -> string
     1.9 -  val mk_list: string list -> string
    1.10 -  val mk_big_list: string list -> string
    1.11 -  val mk_pair: string * string -> string
    1.12 -  val mk_triple: string * string * string -> string
    1.13    type syntax
    1.14    val make_syntax: string list ->
    1.15      (string * (token list -> (string * string) * token list)) list -> syntax
    1.16 @@ -61,6 +55,13 @@
    1.17    val pure_keywords: string list
    1.18    val pure_sections:
    1.19      (string * (token list -> (string * string) * token list)) list
    1.20 +  (*items for building strings*)
    1.21 +  val parens	: string -> string   
    1.22 +  val brackets	: string -> string   
    1.23 +  val mk_list	: string list -> string   
    1.24 +  val mk_big_list : string list -> string   
    1.25 +  val mk_pair	: string * string -> string   
    1.26 +  val mk_triple	: string * string * string -> string   
    1.27  end;
    1.28  
    1.29  functor ThyParseFun(structure Symtab: SYMTAB and ThyScan: THY_SCAN): THY_PARSE =
    1.30 @@ -82,8 +83,8 @@
    1.31  
    1.32  fun eof_err () = error "Unexpected end-of-file";
    1.33  
    1.34 -(*similar to Prolog's cut: reports any syntax error instead of
    1.35 -  backtracking through a superior ||*)
    1.36 +(*Similar to Prolog's cut: reports any syntax error instead of backtracking
    1.37 +  through a superior || *)
    1.38  fun !! parse toks = parse toks
    1.39    handle SYNTAX_ERROR (s1, s2, n) => error ("Syntax error on line " ^
    1.40      string_of_int n ^ ": " ^ s1 ^ " expected and " ^ s2 ^ " was found");