Skip to content

Hyperrefs in table-generator tables #1217

@matthiaskettl

Description

@matthiaskettl

Table generator provides the possibility to include hard-coded hrefs in the table definitions.
Example from SV-COMP:

<?xml version='1.0' ?>
<!DOCTYPE table PUBLIC "+//IDN sosy-lab.org//DTD BenchExec table 1.0//EN"
        "http://www.sosy-lab.org/benchexec/table-1.0.dtd">
<table>
    <!-- .... -->
    <column title="witness" href="PLACEHOLDER">wit</column>
    <column title="inspect witness" href="PLACEHOLDER">inspect</column>
    <!-- .... -->

    <!-- result files -->
</table>

In this case, table generator will create hyperrefs to "PLACEHOLDER" which we have to replace retrospectively and manually with a post-processing script.

It would be convenient to have the possibility to make the href dependent on the value of the current column and row. This could, for example, look like this:

<?xml version='1.0' ?>
<!DOCTYPE table PUBLIC "+//IDN sosy-lab.org//DTD BenchExec table 1.0//EN"
        "http://www.sosy-lab.org/benchexec/table-1.0.dtd">
<table>
    <!-- .... -->
    <column title="witness" href="${value}">wit</column>
    <column title="inspect witness" href="${value}">inspect</column>
    <!-- .... -->

    <!-- result files -->
</table>

Metadata

Metadata

Assignees

No one assigned

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions