54 |
54 |
55 def source(body: XML.Body): XML.Tree = HTML.pre("source", body) |
55 def source(body: XML.Body): XML.Tree = HTML.pre("source", body) |
56 |
56 |
57 def offset_ref(offset: Text.Range): String = |
57 def offset_ref(offset: Text.Range): String = |
58 "offset/" + offset.start + ".." + offset.stop |
58 "offset/" + offset.start + ".." + offset.stop |
59 |
|
60 def export_ref(entity: Entity): String = |
|
61 Export_Theory.export_kind(entity.kind) + "/" + entity.name |
|
62 |
59 |
63 def contents(heading: String, items: List[XML.Body], css_class: String = "contents") |
60 def contents(heading: String, items: List[XML.Body], css_class: String = "contents") |
64 : List[XML.Elem] = |
61 : List[XML.Elem] = |
65 { |
62 { |
66 if (items.isEmpty) Nil |
63 if (items.isEmpty) Nil |
467 val body1 = |
464 val body1 = |
468 if (context.seen_ranges.contains(range)) { |
465 if (context.seen_ranges.contains(range)) { |
469 HTML.entity_def(HTML.span(HTML.id(html_context.offset_ref(range)), body)) |
466 HTML.entity_def(HTML.span(HTML.id(html_context.offset_ref(range)), body)) |
470 } |
467 } |
471 else HTML.span(body) |
468 else HTML.span(body) |
472 entities.map(html_context.export_ref).foldLeft(body1) { |
469 entities.map(_.kname).foldLeft(body1) { |
473 case (elem, id) => HTML.entity_def(HTML.span(HTML.id(id), List(elem))) |
470 case (elem, id) => HTML.entity_def(HTML.span(HTML.id(id), List(elem))) |
474 } |
471 } |
475 } |
472 } |
476 } |
473 } |
477 } |
474 } |
478 |
475 |
479 def entity_ref(thy_name: String, kind: String, name: String): Option[String] = |
476 def entity_ref(thy_name: String, kind: String, name: String): Option[String] = |
480 for { |
477 for { |
481 thy <- theory_by_name.get(thy_name) |
478 thy <- theory_by_name.get(thy_name) |
482 entity <- thy.entity_by_kname.get(Export_Theory.export_kind_name(kind, name)) |
479 entity <- thy.entity_by_kname.get(Export_Theory.export_kind_name(kind, name)) |
483 } yield html_context.export_ref(entity) |
480 } yield entity.kname |
484 |
481 |
485 def offset_ref(context: Entity_Context, thy_name: String, props: Properties.T): Option[String] = |
482 def offset_ref(context: Entity_Context, thy_name: String, props: Properties.T): Option[String] = |
486 { |
483 { |
487 if (thy_name == context.node.theory) { |
484 if (thy_name == context.node.theory) { |
488 for { |
485 for { |