src/Pure/General/markup.scala
author wenzelm
Wed Jun 29 16:31:50 2011 +0200 (2011-06-29 ago)
changeset 43593 11140987d415
parent 43564 9864182c6bad
child 43673 29eb1cd29961
permissions -rw-r--r--
print Path.T with some markup;
     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   /* plain values */
    13 
    14   object Int
    15   {
    16     def apply(x: scala.Int): String = x.toString
    17     def unapply(s: String): Option[scala.Int] =
    18       try { Some(Integer.parseInt(s)) }
    19       catch { case _: NumberFormatException => None }
    20   }
    21 
    22   object Long
    23   {
    24     def apply(x: scala.Long): String = x.toString
    25     def unapply(s: String): Option[scala.Long] =
    26       try { Some(java.lang.Long.parseLong(s)) }
    27       catch { case _: NumberFormatException => None }
    28   }
    29 
    30   object Double
    31   {
    32     def apply(x: scala.Double): String = x.toString
    33     def unapply(s: String): Option[scala.Double] =
    34       try { Some(java.lang.Double.parseDouble(s)) }
    35       catch { case _: NumberFormatException => None }
    36   }
    37 
    38 
    39   /* named properties */
    40 
    41   class Property(val name: String)
    42   {
    43     def apply(value: String): List[(String, String)] = List((name, value))
    44     def unapply(props: List[(String, String)]): Option[String] =
    45       props.find(_._1 == name).map(_._2)
    46   }
    47 
    48   class Int_Property(name: String)
    49   {
    50     def apply(value: scala.Int): List[(String, String)] = List((name, Int(value)))
    51     def unapply(props: List[(String, String)]): Option[Int] =
    52       props.find(_._1 == name) match {
    53         case None => None
    54         case Some((_, value)) => Int.unapply(value)
    55       }
    56   }
    57 
    58   class Long_Property(name: String)
    59   {
    60     def apply(value: scala.Long): List[(String, String)] = List((name, Long(value)))
    61     def unapply(props: List[(String, String)]): Option[Long] =
    62       props.find(_._1 == name) match {
    63         case None => None
    64         case Some((_, value)) => Long.unapply(value)
    65       }
    66   }
    67 
    68   class Double_Property(name: String)
    69   {
    70     def apply(value: scala.Double): List[(String, String)] = List((name, Double(value)))
    71     def unapply(props: List[(String, String)]): Option[Double] =
    72       props.find(_._1 == name) match {
    73         case None => None
    74         case Some((_, value)) => Double.unapply(value)
    75       }
    76   }
    77 
    78 
    79   /* empty */
    80 
    81   val Empty = Markup("", Nil)
    82 
    83 
    84   /* misc properties */
    85 
    86   val NAME = "name"
    87   val Name = new Property(NAME)
    88 
    89   val KIND = "kind"
    90   val Kind = new Property(KIND)
    91 
    92 
    93   /* formal entities */
    94 
    95   val BINDING = "binding"
    96   val ENTITY = "entity"
    97   val DEF = "def"
    98   val REF = "ref"
    99 
   100   object Entity
   101   {
   102     def unapply(markup: Markup): Option[(String, String)] =
   103       markup match {
   104         case Markup(ENTITY, props @ Kind(kind)) =>
   105           props match {
   106             case Name(name) => Some(kind, name)
   107             case _ => None
   108           }
   109         case _ => None
   110       }
   111   }
   112 
   113 
   114   /* position */
   115 
   116   val LINE = "line"
   117   val COLUMN = "column"
   118   val OFFSET = "offset"
   119   val END_OFFSET = "end_offset"
   120   val FILE = "file"
   121   val ID = "id"
   122 
   123   val DEF_LINE = "def_line"
   124   val DEF_COLUMN = "def_column"
   125   val DEF_OFFSET = "def_offset"
   126   val DEF_END_OFFSET = "def_end_offset"
   127   val DEF_FILE = "def_file"
   128   val DEF_ID = "def_id"
   129 
   130   val POSITION_PROPERTIES = Set(LINE, COLUMN, OFFSET, END_OFFSET, FILE, ID)
   131   val POSITION = "position"
   132 
   133 
   134   /* path */
   135 
   136   val PATH = "path"
   137 
   138   object Path
   139   {
   140     def unapply(markup: Markup): Option[String] =
   141       markup match {
   142         case Markup(PATH, Name(name)) => Some(name)
   143         case _ => None
   144       }
   145   }
   146 
   147 
   148   /* pretty printing */
   149 
   150   val Indent = new Int_Property("indent")
   151   val BLOCK = "block"
   152   val Width = new Int_Property("width")
   153   val BREAK = "break"
   154 
   155 
   156   /* hidden text */
   157 
   158   val HIDDEN = "hidden"
   159 
   160 
   161   /* logical entities */
   162 
   163   val CLASS = "class"
   164   val TYPE = "type"
   165   val FIXED = "fixed"
   166   val CONSTANT = "constant"
   167 
   168   val DYNAMIC_FACT = "dynamic_fact"
   169 
   170 
   171   /* inner syntax */
   172 
   173   val TFREE = "tfree"
   174   val TVAR = "tvar"
   175   val FREE = "free"
   176   val SKOLEM = "skolem"
   177   val BOUND = "bound"
   178   val VAR = "var"
   179   val NUM = "num"
   180   val FLOAT = "float"
   181   val XNUM = "xnum"
   182   val XSTR = "xstr"
   183   val LITERAL = "literal"
   184   val DELIMITER = "delimiter"
   185   val INNER_STRING = "inner_string"
   186   val INNER_COMMENT = "inner_comment"
   187 
   188   val TOKEN_RANGE = "token_range"
   189 
   190   val SORT = "sort"
   191   val TYP = "typ"
   192   val TERM = "term"
   193   val PROP = "prop"
   194 
   195   val ATTRIBUTE = "attribute"
   196   val METHOD = "method"
   197 
   198 
   199   /* embedded source text */
   200 
   201   val ML_SOURCE = "ML_source"
   202   val DOC_SOURCE = "doc_source"
   203 
   204   val ANTIQ = "antiq"
   205   val ML_ANTIQUOTATION = "ML antiquotation"
   206   val DOCUMENT_ANTIQUOTATION = "document antiquotation"
   207   val DOCUMENT_ANTIQUOTATION_OPTION = "document antiquotation option"
   208 
   209 
   210   /* ML syntax */
   211 
   212   val ML_KEYWORD = "ML_keyword"
   213   val ML_DELIMITER = "ML_delimiter"
   214   val ML_IDENT = "ML_ident"
   215   val ML_TVAR = "ML_tvar"
   216   val ML_NUMERAL = "ML_numeral"
   217   val ML_CHAR = "ML_char"
   218   val ML_STRING = "ML_string"
   219   val ML_COMMENT = "ML_comment"
   220   val ML_MALFORMED = "ML_malformed"
   221 
   222   val ML_DEF = "ML_def"
   223   val ML_OPEN = "ML_open"
   224   val ML_STRUCT = "ML_struct"
   225   val ML_TYPING = "ML_typing"
   226 
   227 
   228   /* outer syntax */
   229 
   230   val KEYWORD_DECL = "keyword_decl"
   231   val COMMAND_DECL = "command_decl"
   232 
   233   val KEYWORD = "keyword"
   234   val OPERATOR = "operator"
   235   val COMMAND = "command"
   236   val IDENT = "ident"
   237   val STRING = "string"
   238   val ALTSTRING = "altstring"
   239   val VERBATIM = "verbatim"
   240   val COMMENT = "comment"
   241   val CONTROL = "control"
   242   val MALFORMED = "malformed"
   243 
   244   val COMMAND_SPAN = "command_span"
   245   val IGNORED_SPAN = "ignored_span"
   246   val MALFORMED_SPAN = "malformed_span"
   247 
   248 
   249   /* timing */
   250 
   251   val TIMING = "timing"
   252   val ELAPSED = "elapsed"
   253   val CPU = "cpu"
   254   val GC = "gc"
   255 
   256   object Timing
   257   {
   258     def apply(timing: isabelle.Timing): Markup =
   259       Markup(TIMING, List(
   260         (ELAPSED, Double(timing.elapsed.seconds)),
   261         (CPU, Double(timing.cpu.seconds)),
   262         (GC, Double(timing.gc.seconds))))
   263     def unapply(markup: Markup): Option[isabelle.Timing] =
   264       markup match {
   265         case Markup(TIMING, List(
   266           (ELAPSED, Double(elapsed)), (CPU, Double(cpu)), (GC, Double(gc)))) =>
   267             Some(new isabelle.Timing(Time.seconds(elapsed), Time.seconds(cpu), Time.seconds(gc)))
   268         case _ => None
   269       }
   270   }
   271 
   272 
   273   /* toplevel */
   274 
   275   val SUBGOALS = "subgoals"
   276   val PROOF_STATE = "proof_state"
   277 
   278   val STATE = "state"
   279   val SUBGOAL = "subgoal"
   280   val SENDBACK = "sendback"
   281   val HILITE = "hilite"
   282 
   283 
   284   /* command status */
   285 
   286   val TASK = "task"
   287 
   288   val FORKED = "forked"
   289   val JOINED = "joined"
   290   val FAILED = "failed"
   291   val FINISHED = "finished"
   292 
   293 
   294   /* interactive documents */
   295 
   296   val VERSION = "version"
   297   val EXEC = "exec"
   298   val ASSIGN = "assign"
   299   val EDIT = "edit"
   300 
   301 
   302   /* messages */
   303 
   304   val Serial = new Long_Property("serial")
   305 
   306   val MESSAGE = "message"
   307 
   308   val INIT = "init"
   309   val STATUS = "status"
   310   val REPORT = "report"
   311   val WRITELN = "writeln"
   312   val TRACING = "tracing"
   313   val WARNING = "warning"
   314   val ERROR = "error"
   315   val SYSTEM = "system"
   316   val STDOUT = "stdout"
   317   val EXIT = "exit"
   318 
   319   val NO_REPORT = "no_report"
   320 
   321   val BAD = "bad"
   322 
   323   val READY = "ready"
   324 
   325 
   326   /* system data */
   327 
   328   val Data = Markup("data", Nil)
   329 }
   330 
   331 sealed case class Markup(name: String, properties: List[(String, String)])