91 |
91 |
92 |
92 |
93 /* tags */ |
93 /* tags */ |
94 |
94 |
95 object Tags { |
95 object Tags { |
96 object Op extends Enumeration { |
96 enum Op { case fold, drop, keep } |
97 val fold, drop, keep = Value |
|
98 } |
|
99 |
97 |
100 val standard = "document,theory,proof,ML,visible,-invisible,important,unimportant" |
98 val standard = "document,theory,proof,ML,visible,-invisible,important,unimportant" |
101 |
99 |
102 private def explode(spec: String): List[String] = space_explode(',', spec) |
100 private def explode(spec: String): List[String] = space_explode(',', spec) |
103 |
101 |
104 def apply(spec: String): Tags = |
102 def apply(spec: String): Tags = |
105 new Tags(spec, |
103 new Tags(spec, |
106 (explode(standard) ::: explode(spec)).foldLeft(TreeMap.empty[String, Op.Value]) { |
104 (explode(standard) ::: explode(spec)).foldLeft(TreeMap.empty[String, Op]) { |
107 case (m, tag) => |
105 case (m, tag) => |
108 tag.toList match { |
106 tag.toList match { |
109 case '/' :: cs => m + (cs.mkString -> Op.fold) |
107 case '/' :: cs => m + (cs.mkString -> Op.fold) |
110 case '-' :: cs => m + (cs.mkString -> Op.drop) |
108 case '-' :: cs => m + (cs.mkString -> Op.drop) |
111 case '+' :: cs => m + (cs.mkString -> Op.keep) |
109 case '+' :: cs => m + (cs.mkString -> Op.keep) |
114 }) |
112 }) |
115 |
113 |
116 val empty: Tags = apply("") |
114 val empty: Tags = apply("") |
117 } |
115 } |
118 |
116 |
119 class Tags private(spec: String, map: TreeMap[String, Tags.Op.Value]) { |
117 class Tags private(spec: String, map: TreeMap[String, Tags.Op]) { |
120 override def toString: String = spec |
118 override def toString: String = spec |
121 |
119 |
122 def get(name: String): Option[Tags.Op.Value] = map.get(name) |
120 def get(name: String): Option[Tags.Op] = map.get(name) |
123 |
121 |
124 def sty(comment_latex: Boolean): File.Content = { |
122 def sty(comment_latex: Boolean): File.Content = { |
125 val path = Path.explode("isabelletags.sty") |
123 val path = Path.explode("isabelletags.sty") |
126 val comment = |
124 val comment = |
127 if (comment_latex) """\usepackage{comment}""" |
125 if (comment_latex) """\usepackage{comment}""" |