equal
deleted
inserted
replaced
23 /* batch build */ |
23 /* batch build */ |
24 |
24 |
25 object Loading_Theory { |
25 object Loading_Theory { |
26 def unapply(props: Properties.T): Option[(Document.Node.Name, Document_ID.Exec)] = |
26 def unapply(props: Properties.T): Option[(Document.Node.Name, Document_ID.Exec)] = |
27 (props, props, props) match { |
27 (props, props, props) match { |
28 case (Markup.Name(name), Position.File(file), Position.Id(id)) |
28 case (Markup.Name(theory), Position.File(file), Position.Id(id)) |
29 if Path.is_wellformed(file) => Some((Document.Node.Name(file, theory = name), id)) |
29 if Path.is_wellformed(file) => Some((Document.Node.Name(file, theory = theory), id)) |
30 case _ => None |
30 case _ => None |
31 } |
31 } |
32 } |
32 } |
33 |
33 |
34 |
34 |