]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/content_pres/cicNotationLexer.mli
cicUtil: we moved here pp_term from proceduralHelpers
[helm.git] / helm / software / components / content_pres / cicNotationLexer.mli
index cd5f0876dd2fe4d715a5791c27f7f6ffeb7fb5ff..f04575f5f7f7685ddd14c2d981bdc42bec428c7b 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 *)
 
@@ -46,3 +46,5 @@ val remove_level2_ast_keyword: string -> unit (** non idempotent *)
 val is_ligature_char: char -> bool
 val lookup_ligatures: string -> string list
 
+val push: unit -> unit
+val pop: unit -> unit