author  wenzelm 
Wed, 25 Aug 2010 21:31:22 +0200  
changeset 38721  ca8b14fa0d0d 
parent 38474  e498dc2eb576 
child 38722  ba31936497c2 
permissions  rwrr 
27958  1 
/* Title: Pure/General/markup.scala 
2 
Author: Makarius 

3 

4 
Common markup elements. 

5 
*/ 

6 

7 
package isabelle 

8 

27970  9 

32450  10 
object Markup 
11 
{ 

38414
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38355
diff
changeset

12 
/* integers */ 
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38355
diff
changeset

13 

49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38355
diff
changeset

14 
object Int { 
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38355
diff
changeset

15 
def apply(i: scala.Int): String = i.toString 
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38355
diff
changeset

16 
def unapply(s: String): Option[scala.Int] = 
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38355
diff
changeset

17 
try { Some(Integer.parseInt(s)) } 
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38355
diff
changeset

18 
catch { case _: NumberFormatException => None } 
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38355
diff
changeset

19 
} 
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38355
diff
changeset

20 

49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38355
diff
changeset

21 
object Long { 
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38355
diff
changeset

22 
def apply(i: scala.Long): String = i.toString 
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38355
diff
changeset

23 
def unapply(s: String): Option[scala.Long] = 
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38355
diff
changeset

24 
try { Some(java.lang.Long.parseLong(s)) } 
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38355
diff
changeset

25 
catch { case _: NumberFormatException => None } 
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38355
diff
changeset

26 
} 
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38355
diff
changeset

27 

49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38355
diff
changeset

28 

36683  29 
/* property values */ 
30 

31 
def get_string(name: String, props: List[(String, String)]): Option[String] = 

32 
props.find(p => p._1 == name).map(_._2) 

33 

38414
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38355
diff
changeset

34 
def get_long(name: String, props: List[(String, String)]): Option[scala.Long] = 
38355
8cb265fb12fe
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);
wenzelm
parents:
38259
diff
changeset

35 
{ 
8cb265fb12fe
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);
wenzelm
parents:
38259
diff
changeset

36 
get_string(name, props) match { 
8cb265fb12fe
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);
wenzelm
parents:
38259
diff
changeset

37 
case None => None 
38414
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38355
diff
changeset

38 
case Some(Long(i)) => Some(i) 
38355
8cb265fb12fe
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);
wenzelm
parents:
38259
diff
changeset

39 
} 
8cb265fb12fe
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);
wenzelm
parents:
38259
diff
changeset

40 
} 
8cb265fb12fe
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);
wenzelm
parents:
38259
diff
changeset

41 

38414
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38355
diff
changeset

42 
def get_int(name: String, props: List[(String, String)]): Option[scala.Int] = 
36683  43 
{ 
44 
get_string(name, props) match { 

45 
case None => None 

38414
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38355
diff
changeset

46 
case Some(Int(i)) => Some(i) 
36683  47 
} 
48 
} 

49 

50 

38474
e498dc2eb576
uniform Markup.empty/Markup.Empty in ML and Scala;
wenzelm
parents:
38429
diff
changeset

51 
/* empty */ 
e498dc2eb576
uniform Markup.empty/Markup.Empty in ML and Scala;
wenzelm
parents:
38429
diff
changeset

52 

e498dc2eb576
uniform Markup.empty/Markup.Empty in ML and Scala;
wenzelm
parents:
38429
diff
changeset

53 
val Empty = Markup("", Nil) 
e498dc2eb576
uniform Markup.empty/Markup.Empty in ML and Scala;
wenzelm
parents:
38429
diff
changeset

54 

e498dc2eb576
uniform Markup.empty/Markup.Empty in ML and Scala;
wenzelm
parents:
38429
diff
changeset

55 

38721
ca8b14fa0d0d
added some proof state markup, notably number of subgoals (e.g. for indentation);
wenzelm
parents:
38474
diff
changeset

56 
/* misc properties */ 
29184  57 

58 
val NAME = "name" 

59 
val KIND = "kind" 

60 

61 

33088
757d7787b10c
markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents:
32450
diff
changeset

62 
/* formal entities */ 
757d7787b10c
markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents:
32450
diff
changeset

63 

757d7787b10c
markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents:
32450
diff
changeset

64 
val ENTITY = "entity" 
757d7787b10c
markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents:
32450
diff
changeset

65 
val DEF = "def" 
757d7787b10c
markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents:
32450
diff
changeset

66 
val REF = "ref" 
757d7787b10c
markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents:
32450
diff
changeset

67 

757d7787b10c
markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents:
32450
diff
changeset

68 

27970  69 
/* position */ 
70 

71 
val LINE = "line" 

72 
val COLUMN = "column" 

73 
val OFFSET = "offset" 

74 
val END_LINE = "end_line" 

75 
val END_COLUMN = "end_column" 

76 
val END_OFFSET = "end_offset" 

77 
val FILE = "file" 

78 
val ID = "id" 

79 

32450  80 
val POSITION_PROPERTIES = 
81 
Set(LINE, COLUMN, OFFSET, END_LINE, END_COLUMN, END_OFFSET, FILE, ID) 

29205  82 

29184  83 
val POSITION = "position" 
84 
val LOCATION = "location" 

85 

86 

36683  87 
/* pretty printing */ 
88 

89 
val INDENT = "indent" 

90 
val BLOCK = "block" 

91 
val WIDTH = "width" 

92 
val BREAK = "break" 

93 

94 

33985  95 
/* hidden text */ 
96 

97 
val HIDDEN = "hidden" 

98 

99 

29184  100 
/* logical entities */ 
101 

102 
val TCLASS = "tclass" 

103 
val TYCON = "tycon" 

104 
val FIXED_DECL = "fixed_decl" 

105 
val FIXED = "fixed" 

106 
val CONST_DECL = "const_decl" 

107 
val CONST = "const" 

108 
val FACT_DECL = "fact_decl" 

109 
val FACT = "fact" 

110 
val DYNAMIC_FACT = "dynamic_fact" 

111 
val LOCAL_FACT_DECL = "local_fact_decl" 

112 
val LOCAL_FACT = "local_fact" 

113 

114 

115 
/* inner syntax */ 

116 

117 
val TFREE = "tfree" 

118 
val TVAR = "tvar" 

119 
val FREE = "free" 

120 
val SKOLEM = "skolem" 

121 
val BOUND = "bound" 

122 
val VAR = "var" 

123 
val NUM = "num" 

124 
val FLOAT = "float" 

125 
val XNUM = "xnum" 

126 
val XSTR = "xstr" 

127 
val LITERAL = "literal" 

128 
val INNER_COMMENT = "inner_comment" 

129 

130 
val SORT = "sort" 

131 
val TYP = "typ" 

132 
val TERM = "term" 

133 
val PROP = "prop" 

134 

135 
val ATTRIBUTE = "attribute" 

136 
val METHOD = "method" 

137 

138 

139 
/* embedded source text */ 

140 

141 
val ML_SOURCE = "ML_source" 

142 
val DOC_SOURCE = "doc_source" 

143 

144 
val ANTIQ = "antiq" 

145 
val ML_ANTIQ = "ML_antiq" 

146 
val DOC_ANTIQ = "doc_antiq" 

147 

148 

30615  149 
/* ML syntax */ 
150 

151 
val ML_KEYWORD = "ML_keyword" 

37195  152 
val ML_DELIMITER = "ML_delimiter" 
30615  153 
val ML_IDENT = "ML_ident" 
154 
val ML_TVAR = "ML_tvar" 

155 
val ML_NUMERAL = "ML_numeral" 

156 
val ML_CHAR = "ML_char" 

157 
val ML_STRING = "ML_string" 

158 
val ML_COMMENT = "ML_comment" 

159 
val ML_MALFORMED = "ML_malformed" 

160 

30702  161 
val ML_DEF = "ML_def" 
31472  162 
val ML_OPEN = "ML_open" 
163 
val ML_STRUCT = "ML_struct" 

30702  164 
val ML_REF = "ML_ref" 
165 
val ML_TYPING = "ML_typing" 

166 

30615  167 

29184  168 
/* outer syntax */ 
169 

170 
val KEYWORD_DECL = "keyword_decl" 

171 
val COMMAND_DECL = "command_decl" 

172 

173 
val KEYWORD = "keyword" 

37194  174 
val OPERATOR = "operator" 
29184  175 
val COMMAND = "command" 
176 
val IDENT = "ident" 

177 
val STRING = "string" 

178 
val ALTSTRING = "altstring" 

179 
val VERBATIM = "verbatim" 

180 
val COMMENT = "comment" 

181 
val CONTROL = "control" 

182 
val MALFORMED = "malformed" 

183 

29185  184 
val COMMAND_SPAN = "command_span" 
185 
val IGNORED_SPAN = "ignored_span" 

186 
val MALFORMED_SPAN = "malformed_span" 

187 

29184  188 

189 
/* toplevel */ 

190 

38721
ca8b14fa0d0d
added some proof state markup, notably number of subgoals (e.g. for indentation);
wenzelm
parents:
38474
diff
changeset

191 
val SUBGOALS = "subgoals" 
ca8b14fa0d0d
added some proof state markup, notably number of subgoals (e.g. for indentation);
wenzelm
parents:
38474
diff
changeset

192 
val PROOF_STATE = "proof_state" 
ca8b14fa0d0d
added some proof state markup, notably number of subgoals (e.g. for indentation);
wenzelm
parents:
38474
diff
changeset

193 

29184  194 
val STATE = "state" 
195 
val SUBGOAL = "subgoal" 

196 
val SENDBACK = "sendback" 

197 
val HILITE = "hilite" 

198 

199 

200 
/* command status */ 

201 

29417  202 
val TASK = "task" 
203 

37186
349e9223c685
explicit markup for forked goals, as indicated by Goal.fork;
wenzelm
parents:
37121
diff
changeset

204 
val FORKED = "forked" 
349e9223c685
explicit markup for forked goals, as indicated by Goal.fork;
wenzelm
parents:
37121
diff
changeset

205 
val JOINED = "joined" 
29184  206 
val FAILED = "failed" 
207 
val FINISHED = "finished" 

29488  208 

209 

210 
/* interactive documents */ 

211 

38414
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38355
diff
changeset

212 
val VERSION = "version" 
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38355
diff
changeset

213 
val EXEC = "exec" 
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38355
diff
changeset

214 
val ASSIGN = "assign" 
29488  215 
val EDIT = "edit" 
29184  216 

27970  217 

218 
/* messages */ 

219 

220 
val PID = "pid" 

221 

29195  222 
val MESSAGE = "message" 
29522
793766d4c1b5
moved message markup into Scala layer  reduced redundancy;
wenzelm
parents:
29488
diff
changeset

223 
val CLASS = "class" 
793766d4c1b5
moved message markup into Scala layer  reduced redundancy;
wenzelm
parents:
29488
diff
changeset

224 

793766d4c1b5
moved message markup into Scala layer  reduced redundancy;
wenzelm
parents:
29488
diff
changeset

225 
val INIT = "init" 
793766d4c1b5
moved message markup into Scala layer  reduced redundancy;
wenzelm
parents:
29488
diff
changeset

226 
val STATUS = "status" 
38236
d8c7be27e01d
explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
wenzelm
parents:
38231
diff
changeset

227 
val REPORT = "report" 
29522
793766d4c1b5
moved message markup into Scala layer  reduced redundancy;
wenzelm
parents:
29488
diff
changeset

228 
val WRITELN = "writeln" 
793766d4c1b5
moved message markup into Scala layer  reduced redundancy;
wenzelm
parents:
29488
diff
changeset

229 
val TRACING = "tracing" 
793766d4c1b5
moved message markup into Scala layer  reduced redundancy;
wenzelm
parents:
29488
diff
changeset

230 
val WARNING = "warning" 
793766d4c1b5
moved message markup into Scala layer  reduced redundancy;
wenzelm
parents:
29488
diff
changeset

231 
val ERROR = "error" 
793766d4c1b5
moved message markup into Scala layer  reduced redundancy;
wenzelm
parents:
29488
diff
changeset

232 
val DEBUG = "debug" 
793766d4c1b5
moved message markup into Scala layer  reduced redundancy;
wenzelm
parents:
29488
diff
changeset

233 
val SYSTEM = "system" 
38259
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38236
diff
changeset

234 
val INPUT = "input" 
29522
793766d4c1b5
moved message markup into Scala layer  reduced redundancy;
wenzelm
parents:
29488
diff
changeset

235 
val STDIN = "stdin" 
793766d4c1b5
moved message markup into Scala layer  reduced redundancy;
wenzelm
parents:
29488
diff
changeset

236 
val STDOUT = "stdout" 
793766d4c1b5
moved message markup into Scala layer  reduced redundancy;
wenzelm
parents:
29488
diff
changeset

237 
val SIGNAL = "signal" 
793766d4c1b5
moved message markup into Scala layer  reduced redundancy;
wenzelm
parents:
29488
diff
changeset

238 
val EXIT = "exit" 
29195  239 

38231  240 
val Ready = Markup("ready", Nil) 
31384
ce169bd37fc0
IsabelleProcess: emit status "ready" after initialization and reports;
wenzelm
parents:
30702
diff
changeset

241 

27970  242 

34119  243 
/* system data */ 
27970  244 

38231  245 
val Data = Markup("data", Nil) 
27958  246 
} 
38230
ed147003de4b
simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
wenzelm
parents:
37195
diff
changeset

247 

ed147003de4b
simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
wenzelm
parents:
37195
diff
changeset

248 
sealed case class Markup(name: String, properties: List[(String, String)]) 