|
1 /* Title: Pure/Thy/export_theory.scala |
|
2 Author: Makarius |
|
3 |
|
4 Export foundational theory content. |
|
5 */ |
|
6 |
|
7 package isabelle |
|
8 |
|
9 |
|
10 object Export_Theory |
|
11 { |
|
12 /* entities */ |
|
13 |
|
14 sealed case class Entity(name: String, kind: String, serial: Long, pos: Position.T) |
|
15 { |
|
16 override def toString: String = name |
|
17 } |
|
18 |
|
19 def decode_entity(tree: XML.Tree): (Entity, XML.Body) = |
|
20 { |
|
21 def err(): Nothing = throw new XML.XML_Body(List(tree)) |
|
22 |
|
23 tree match { |
|
24 case XML.Elem(Markup(Markup.ENTITY, props), body) => |
|
25 val name = Markup.Name.unapply(props) getOrElse err() |
|
26 val kind = Markup.Kind.unapply(props) getOrElse err() |
|
27 val serial = Markup.Serial.unapply(props) getOrElse err() |
|
28 val pos = props.filter({ case (a, _) => Markup.POSITION_PROPERTIES(a) }) |
|
29 (Entity(name, kind, serial, pos), body) |
|
30 case _ => err() |
|
31 } |
|
32 } |
|
33 |
|
34 |
|
35 /* types */ |
|
36 |
|
37 sealed case class Type(entity: Entity, args: List[String], abbrev: Option[Term.Typ]) |
|
38 { |
|
39 def arity: Int = args.length |
|
40 } |
|
41 |
|
42 def decode_type(tree: XML.Tree): Type = |
|
43 { |
|
44 val (entity, body) = decode_entity(tree) |
|
45 val (args, abbrev) = |
|
46 { |
|
47 import XML.Decode._ |
|
48 pair(list(string), option(Term_XML.Decode.typ))(body) |
|
49 } |
|
50 Type(entity, args, abbrev) |
|
51 } |
|
52 |
|
53 |
|
54 /* consts */ |
|
55 |
|
56 sealed case class Const(entity: Entity, typ: Term.Typ, abbrev: Option[Term.Term]) |
|
57 |
|
58 def decode_const(tree: XML.Tree): Const = |
|
59 { |
|
60 val (entity, body) = decode_entity(tree) |
|
61 val (typ, abbrev) = |
|
62 { |
|
63 import XML.Decode._ |
|
64 pair(Term_XML.Decode.typ, option(Term_XML.Decode.term))(body) |
|
65 } |
|
66 Const(entity, typ, abbrev) |
|
67 } |
|
68 } |