]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/content_pres/cicNotationLexer.mli
made executable again
[helm.git] / helm / software / components / content_pres / cicNotationLexer.mli
index cd5f0876dd2fe4d715a5791c27f7f6ffeb7fb5ff..1edacd96097139dcfee979838ef9781d949414a0 100644 (file)
@@ -32,9 +32,9 @@ exception Error of int * int * string
    * passing values of type char Stream.t, they should be in fact Ulexing.lexbuf
    * casted with Obj.magic :-/ Read the comment in the .ml for the rationale *)
 
-val level1_pattern_lexer: (string * string) Token.glexer
-val level2_ast_lexer: (string * string) Token.glexer
-val level2_meta_lexer: (string * string) Token.glexer
+val level1_pattern_lexer: unit -> (string * string) Token.glexer
+val level2_ast_lexer: unit -> (string * string) Token.glexer
+val level2_meta_lexer: unit -> (string * string) Token.glexer
 
   (** XXX ZACK DEFCON 4 END *)
 
@@ -43,6 +43,5 @@ val remove_level2_ast_keyword: string -> unit (** non idempotent *)
 
 (** {2 Ligatures} *)
 
-val is_ligature_char: char -> bool
-val lookup_ligatures: string -> string list
-
+val push: unit -> unit
+val pop: unit -> unit