777 if (cite_commands.contains(name)) cite_antiquotation(name, body2) |
777 if (cite_commands.contains(name)) cite_antiquotation(name, body2) |
778 else cite_antiquotation(CITE, body2 + " using " + quote(name)) |
778 else cite_antiquotation(CITE, body2 + " using " + quote(name)) |
779 } |
779 } |
780 } |
780 } |
781 |
781 |
782 object Cite_Parsers extends Parse.Parsers { |
|
783 val keywords: Keyword.Keywords = Thy_Header.bootstrap_keywords + "in" + "and" + "using" |
|
784 |
|
785 val location: Parser[String] = embedded ~ $$$("in") ^^ { case x ~ _ => x } | success("") |
|
786 val citations: Parser[String] = rep1sep(name, $$$("and")) ^^ (x => x.mkString(",")) |
|
787 val kind: Parser[String] = $$$("using") ~! name ^^ { case _ ~ x => x } | success(CITE) |
|
788 |
|
789 val nocite: Parser[Latex.Text] = |
|
790 location ~ citations ~ kind ^^ { case _ ~ x ~ _ => |
|
791 List(XML.elem(Markup.Latex_Cite(Markup.Kind(NOCITE) ::: Markup.Citations(x)))) |
|
792 } |
|
793 } |
|
794 |
|
795 |
782 |
796 /* parse within raw source */ |
783 /* parse within raw source */ |
|
784 |
|
785 object Cite { |
|
786 object Parsers extends Parse.Parsers { |
|
787 val keywords: Keyword.Keywords = Thy_Header.bootstrap_keywords + "in" + "and" + "using" |
|
788 |
|
789 val location: Parser[String] = embedded ~ $$$("in") ^^ { case x ~ _ => x } | success("") |
|
790 val citations: Parser[String] = rep1sep(name, $$$("and")) ^^ (x => x.mkString(",")) |
|
791 val kind: Parser[String] = $$$("using") ~! name ^^ { case _ ~ x => x } | success(CITE) |
|
792 |
|
793 val nocite: Parser[Latex.Text] = |
|
794 location ~ citations ~ kind ^^ { case _ ~ x ~ _ => |
|
795 List(XML.elem(Markup.Latex_Cite(Markup.Kind(NOCITE) ::: Markup.Citations(x)))) |
|
796 } |
|
797 } |
|
798 |
|
799 def parse( |
|
800 cite_commands: List[String], |
|
801 text: String, |
|
802 start: Isar_Token.Pos = Isar_Token.Pos.start |
|
803 ): List[Cite] = { |
|
804 val controls = cite_commands.map(s => Symbol.control_prefix + s + Symbol.control_suffix) |
|
805 val special = (controls ::: controls.map(Symbol.decode)).toSet |
|
806 |
|
807 val Parsers = Antiquote.Parsers |
|
808 Parsers.parseAll(Parsers.rep(Parsers.antiquote_special(special)), text) match { |
|
809 case Parsers.Success(ants, _) => |
|
810 var pos = start |
|
811 val result = new mutable.ListBuffer[Cite] |
|
812 for (ant <- ants) { |
|
813 ant match { |
|
814 case Antiquote.Control(source) => |
|
815 for { |
|
816 head <- Symbol.iterator(source).nextOption |
|
817 kind <- Symbol.control_name(Symbol.encode(head)) |
|
818 } { |
|
819 val rest = source.substring(head.length) |
|
820 val (body, pos1) = |
|
821 if (rest.isEmpty) (rest, pos) |
|
822 else (Scan.Parsers.cartouche_content(rest), pos.advance(Symbol.open)) |
|
823 result += Cite(kind, body, pos1) |
|
824 } |
|
825 case _ => |
|
826 } |
|
827 pos = pos.advance(ant.source) |
|
828 } |
|
829 result.toList |
|
830 case _ => error("Unexpected failure parsing special antiquotations:\n" + text) |
|
831 } |
|
832 } |
|
833 |
|
834 def parse_latex( |
|
835 cite_commands: List[String], |
|
836 text: String, |
|
837 start: Isar_Token.Pos = Isar_Token.Pos.start |
|
838 ): Latex.Text = parse(cite_commands, text, start = start).flatMap(_.nocite_latex) |
|
839 } |
797 |
840 |
798 sealed case class Cite(kind: String, body: String, pos: Isar_Token.Pos) { |
841 sealed case class Cite(kind: String, body: String, pos: Isar_Token.Pos) { |
799 def position: Position.T = pos.position() |
842 def position: Position.T = pos.position() |
800 |
843 |
801 def nocite_latex: Latex.Text = { |
844 def nocite_latex: Latex.Text = { |
802 val Parsers = Cite_Parsers |
845 val Parsers = Cite.Parsers |
803 val tokens = Isar_Token.explode(Parsers.keywords, body) |
846 val tokens = Isar_Token.explode(Parsers.keywords, body) |
804 Parsers.parse_all(Parsers.nocite, Isar_Token.reader(tokens, pos)) match { |
847 Parsers.parse_all(Parsers.nocite, Isar_Token.reader(tokens, pos)) match { |
805 case Parsers.Success(nocite, _) => List(XML.Elem(Markup.Latex_Output(position), nocite)) |
848 case Parsers.Success(nocite, _) => List(XML.Elem(Markup.Latex_Output(position), nocite)) |
806 case _ => Nil |
849 case _ => Nil |
807 } |
850 } |
809 |
852 |
810 def errors: List[String] = |
853 def errors: List[String] = |
811 if (nocite_latex.nonEmpty) Nil |
854 if (nocite_latex.nonEmpty) Nil |
812 else List("Malformed citation" + Position.here(position)) |
855 else List("Malformed citation" + Position.here(position)) |
813 } |
856 } |
814 |
|
815 def parse_citations( |
|
816 cite_commands: List[String], |
|
817 text: String, |
|
818 start: Isar_Token.Pos = Isar_Token.Pos.start |
|
819 ): List[Cite] = { |
|
820 val controls = cite_commands.map(s => Symbol.control_prefix + s + Symbol.control_suffix) |
|
821 val special = (controls ::: controls.map(Symbol.decode)).toSet |
|
822 |
|
823 val Parsers = Antiquote.Parsers |
|
824 Parsers.parseAll(Parsers.rep(Parsers.antiquote_special(special)), text) match { |
|
825 case Parsers.Success(ants, _) => |
|
826 var pos = start |
|
827 val result = new mutable.ListBuffer[Cite] |
|
828 for (ant <- ants) { |
|
829 ant match { |
|
830 case Antiquote.Control(source) => |
|
831 for { |
|
832 head <- Symbol.iterator(source).nextOption |
|
833 kind <- Symbol.control_name(Symbol.encode(head)) |
|
834 } { |
|
835 val rest = source.substring(head.length) |
|
836 val (body, pos1) = |
|
837 if (rest.isEmpty) (rest, pos) |
|
838 else (Scan.Parsers.cartouche_content(rest), pos.advance(Symbol.open)) |
|
839 result += Cite(kind, body, pos1) |
|
840 } |
|
841 case _ => |
|
842 } |
|
843 pos = pos.advance(ant.source) |
|
844 } |
|
845 result.toList |
|
846 case _ => error("Unexpected failure parsing special antiquotations:\n" + text) |
|
847 } |
|
848 } |
|
849 |
|
850 def parse_citations_latex( |
|
851 cite_commands: List[String], |
|
852 text: String, |
|
853 start: Isar_Token.Pos = Isar_Token.Pos.start |
|
854 ): Latex.Text = parse_citations(cite_commands, text, start = start).flatMap(_.nocite_latex) |
|
855 } |
857 } |