wenzelm@52530: (* Title: Pure/PIDE/document_id.ML wenzelm@52530: Author: Makarius wenzelm@52530: wenzelm@52530: Unique identifiers for document structure. wenzelm@52530: wenzelm@52530: NB: ML ticks forwards > 0, JVM ticks backwards < 0. wenzelm@52530: *) wenzelm@52530: wenzelm@52530: signature DOCUMENT_ID = wenzelm@52530: sig wenzelm@52531: type generic = int wenzelm@52531: type version = generic wenzelm@52531: type command = generic wenzelm@52531: type exec = generic wenzelm@52606: type execution = generic wenzelm@52531: val none: generic wenzelm@52531: val make: unit -> generic wenzelm@52531: val parse: string -> generic wenzelm@52531: val print: generic -> string wenzelm@52530: end; wenzelm@52530: wenzelm@52530: structure Document_ID: DOCUMENT_ID = wenzelm@52530: struct wenzelm@52530: wenzelm@52531: type generic = int; wenzelm@52531: type version = generic; wenzelm@52531: type command = generic; wenzelm@52531: type exec = generic; wenzelm@52606: type execution = generic; wenzelm@52530: wenzelm@52530: val none = 0; wenzelm@52537: val make = Counter.make (); wenzelm@52530: wenzelm@63806: val parse = Value.parse_int; wenzelm@63806: val print = Value.print_int; wenzelm@52530: wenzelm@52530: end; wenzelm@52530: