src/Pure/PIDE/document_id.scala
author wenzelm
Sat Mar 01 22:46:31 2014 +0100 (2014-03-01)
changeset 55828 42ac3cfb89f6
parent 52537 4b5941730bd8
child 56744 0b74d1df4b8e
permissions -rw-r--r--
clarified language markup: added "delimited" property;
type Symbol_Pos.source preserves information about delimited outer tokens (e.g string, cartouche);
observe Completion.Language_Context only for delimited languages, which is important to complete keywords after undelimited inner tokens, e.g. "lemma A pro";
wenzelm@52530
     1
/*  Title:      Pure/PIDE/document_id.scala
wenzelm@52530
     2
    Author:     Makarius
wenzelm@52530
     3
wenzelm@52530
     4
Unique identifiers for document structure.
wenzelm@52530
     5
wenzelm@52530
     6
NB: ML ticks forwards > 0, JVM ticks backwards < 0.
wenzelm@52530
     7
*/
wenzelm@52530
     8
wenzelm@52530
     9
package isabelle
wenzelm@52530
    10
wenzelm@52530
    11
wenzelm@52530
    12
object Document_ID
wenzelm@52530
    13
{
wenzelm@52531
    14
  type Generic = Long
wenzelm@52531
    15
  type Version = Generic
wenzelm@52531
    16
  type Command = Generic
wenzelm@52531
    17
  type Exec = Generic
wenzelm@52530
    18
wenzelm@52531
    19
  val none: Generic = 0
wenzelm@52537
    20
  val make = Counter.make()
wenzelm@52530
    21
wenzelm@52531
    22
  def apply(id: Generic): String = Properties.Value.Long.apply(id)
wenzelm@52531
    23
  def unapply(s: String): Option[Generic] = Properties.Value.Long.unapply(s)
wenzelm@52530
    24
}
wenzelm@52530
    25