equal
deleted
inserted
replaced
65 |
65 |
66 val POSITION_PROPERTIES = Set(LINE, OFFSET, END_OFFSET, FILE, ID) |
66 val POSITION_PROPERTIES = Set(LINE, OFFSET, END_OFFSET, FILE, ID) |
67 val POSITION = "position" |
67 val POSITION = "position" |
68 |
68 |
69 |
69 |
70 /* path */ |
70 /* external resources */ |
71 |
71 |
72 val PATH = "path" |
72 val PATH = "path" |
73 |
73 |
74 object Path |
74 object Path |
75 { |
75 { |
76 def unapply(markup: Markup): Option[String] = |
76 def unapply(markup: Markup): Option[String] = |
77 markup match { |
77 markup match { |
78 case Markup(PATH, Name(name)) => Some(name) |
78 case Markup(PATH, Name(name)) => Some(name) |
|
79 case _ => None |
|
80 } |
|
81 } |
|
82 |
|
83 val URL = "url" |
|
84 |
|
85 object Url |
|
86 { |
|
87 def unapply(markup: Markup): Option[String] = |
|
88 markup match { |
|
89 case Markup(URL, Name(name)) => Some(name) |
79 case _ => None |
90 case _ => None |
80 } |
91 } |
81 } |
92 } |
82 |
93 |
83 |
94 |