src/Pure/General/markup.scala
author wenzelm
Wed Aug 11 22:41:26 2010 +0200 (2010-08-11)
changeset 38355 8cb265fb12fe
parent 38259 2b61c5e27399
child 38414 49f1f657adc2
permissions -rw-r--r--
represent document ids by (long) int, to benefit from the somewhat faster Inttab in ML (LinearSet in Scala is invariably indexed by native object ids);
     1 /*  Title:      Pure/General/markup.scala
     2     Author:     Makarius
     3 
     4 Common markup elements.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 object Markup
    11 {
    12   /* property values */
    13 
    14   def get_string(name: String, props: List[(String, String)]): Option[String] =
    15     props.find(p => p._1 == name).map(_._2)
    16 
    17 
    18   def parse_long(s: String): Option[Long] =
    19     try { Some(java.lang.Long.parseLong(s)) }
    20     catch { case _: NumberFormatException => None }
    21 
    22   def get_long(name: String, props: List[(String, String)]): Option[Long] =
    23   {
    24     get_string(name, props) match {
    25       case None => None
    26       case Some(value) => parse_long(value)
    27     }
    28   }
    29 
    30 
    31   def parse_int(s: String): Option[Int] =
    32     try { Some(Integer.parseInt(s)) }
    33     catch { case _: NumberFormatException => None }
    34 
    35   def get_int(name: String, props: List[(String, String)]): Option[Int] =
    36   {
    37     get_string(name, props) match {
    38       case None => None
    39       case Some(value) => parse_int(value)
    40     }
    41   }
    42 
    43 
    44   /* name */
    45 
    46   val NAME = "name"
    47   val KIND = "kind"
    48 
    49 
    50   /* formal entities */
    51 
    52   val ENTITY = "entity"
    53   val DEF = "def"
    54   val REF = "ref"
    55 
    56 
    57   /* position */
    58 
    59   val LINE = "line"
    60   val COLUMN = "column"
    61   val OFFSET = "offset"
    62   val END_LINE = "end_line"
    63   val END_COLUMN = "end_column"
    64   val END_OFFSET = "end_offset"
    65   val FILE = "file"
    66   val ID = "id"
    67 
    68   val POSITION_PROPERTIES =
    69     Set(LINE, COLUMN, OFFSET, END_LINE, END_COLUMN, END_OFFSET, FILE, ID)
    70 
    71   val POSITION = "position"
    72   val LOCATION = "location"
    73 
    74 
    75   /* pretty printing */
    76 
    77   val INDENT = "indent"
    78   val BLOCK = "block"
    79   val WIDTH = "width"
    80   val BREAK = "break"
    81 
    82 
    83   /* hidden text */
    84 
    85   val HIDDEN = "hidden"
    86 
    87 
    88   /* logical entities */
    89 
    90   val TCLASS = "tclass"
    91   val TYCON = "tycon"
    92   val FIXED_DECL = "fixed_decl"
    93   val FIXED = "fixed"
    94   val CONST_DECL = "const_decl"
    95   val CONST = "const"
    96   val FACT_DECL = "fact_decl"
    97   val FACT = "fact"
    98   val DYNAMIC_FACT = "dynamic_fact"
    99   val LOCAL_FACT_DECL = "local_fact_decl"
   100   val LOCAL_FACT = "local_fact"
   101 
   102 
   103   /* inner syntax */
   104 
   105   val TFREE = "tfree"
   106   val TVAR = "tvar"
   107   val FREE = "free"
   108   val SKOLEM = "skolem"
   109   val BOUND = "bound"
   110   val VAR = "var"
   111   val NUM = "num"
   112   val FLOAT = "float"
   113   val XNUM = "xnum"
   114   val XSTR = "xstr"
   115   val LITERAL = "literal"
   116   val INNER_COMMENT = "inner_comment"
   117 
   118   val SORT = "sort"
   119   val TYP = "typ"
   120   val TERM = "term"
   121   val PROP = "prop"
   122 
   123   val ATTRIBUTE = "attribute"
   124   val METHOD = "method"
   125 
   126 
   127   /* embedded source text */
   128 
   129   val ML_SOURCE = "ML_source"
   130   val DOC_SOURCE = "doc_source"
   131 
   132   val ANTIQ = "antiq"
   133   val ML_ANTIQ = "ML_antiq"
   134   val DOC_ANTIQ = "doc_antiq"
   135 
   136 
   137   /* ML syntax */
   138 
   139   val ML_KEYWORD = "ML_keyword"
   140   val ML_DELIMITER = "ML_delimiter"
   141   val ML_IDENT = "ML_ident"
   142   val ML_TVAR = "ML_tvar"
   143   val ML_NUMERAL = "ML_numeral"
   144   val ML_CHAR = "ML_char"
   145   val ML_STRING = "ML_string"
   146   val ML_COMMENT = "ML_comment"
   147   val ML_MALFORMED = "ML_malformed"
   148 
   149   val ML_DEF = "ML_def"
   150   val ML_OPEN = "ML_open"
   151   val ML_STRUCT = "ML_struct"
   152   val ML_REF = "ML_ref"
   153   val ML_TYPING = "ML_typing"
   154 
   155 
   156   /* outer syntax */
   157 
   158   val KEYWORD_DECL = "keyword_decl"
   159   val COMMAND_DECL = "command_decl"
   160 
   161   val KEYWORD = "keyword"
   162   val OPERATOR = "operator"
   163   val COMMAND = "command"
   164   val IDENT = "ident"
   165   val STRING = "string"
   166   val ALTSTRING = "altstring"
   167   val VERBATIM = "verbatim"
   168   val COMMENT = "comment"
   169   val CONTROL = "control"
   170   val MALFORMED = "malformed"
   171 
   172   val COMMAND_SPAN = "command_span"
   173   val IGNORED_SPAN = "ignored_span"
   174   val MALFORMED_SPAN = "malformed_span"
   175 
   176 
   177   /* toplevel */
   178 
   179   val STATE = "state"
   180   val SUBGOAL = "subgoal"
   181   val SENDBACK = "sendback"
   182   val HILITE = "hilite"
   183 
   184 
   185   /* command status */
   186 
   187   val TASK = "task"
   188 
   189   val UNPROCESSED = "unprocessed"
   190   val RUNNING = "running"
   191   val FORKED = "forked"
   192   val JOINED = "joined"
   193   val FAILED = "failed"
   194   val FINISHED = "finished"
   195   val DISPOSED = "disposed"
   196 
   197 
   198   /* interactive documents */
   199 
   200   val Assign = Markup("assign", Nil)
   201   val EDIT = "edit"
   202 
   203 
   204   /* messages */
   205 
   206   val PID = "pid"
   207 
   208   val MESSAGE = "message"
   209   val CLASS = "class"
   210 
   211   val INIT = "init"
   212   val STATUS = "status"
   213   val REPORT = "report"
   214   val WRITELN = "writeln"
   215   val TRACING = "tracing"
   216   val WARNING = "warning"
   217   val ERROR = "error"
   218   val DEBUG = "debug"
   219   val SYSTEM = "system"
   220   val INPUT = "input"
   221   val STDIN = "stdin"
   222   val STDOUT = "stdout"
   223   val SIGNAL = "signal"
   224   val EXIT = "exit"
   225 
   226   val Ready = Markup("ready", Nil)
   227 
   228 
   229   /* system data */
   230 
   231   val Data = Markup("data", Nil)
   232 }
   233 
   234 sealed case class Markup(name: String, properties: List[(String, String)])