Typed bindings as an alternative approach to smart-ref

#1

Currently, smart-ref uses the name of labels to determine whether the reference is a theorem, a lemma, or whatever.

I am trying to understand the possibility of an alternative approach in terms of some sort of typed bindings. I imagine that it is implemented as follows:

  1. Typed bindings have a “type” and the binding itself;
  2. get-typed-binding will return both the type and the binding if it is typed;
  3. get-binding will return only the binding;
  4. set-typed-binding will set a typed binding;
  5. Modify the macros such as next-theorem which will invoke set-typed-binding instead;
  6. smart-ref analyzes the types in the typed binding, instead of the label name.

I am not sure how to implement this properly. For example, whether it is better to write this in macro or Scheme codes?

2 Likes
#2

I tend to prefer easy approached. The minimal one that I see is to require that labels have the format type:id, e.g. theorem:one and enforce that the type can be chosen only from a limited class. From this is easy to go on.

#3

This is how smart-ref is implemented. The issue is that, once I want to upgrade a lemma to a proposition or a theorem, I have to simultaneously modify the environment, the label, and all references. It is not difficult (and is what I am doing now), but cumbersome.

1 Like
#4

I see your point and I agree. Maybe one cans (with some scheme) to infer the innermost relevant environment at the locus where a binding is set, and put the result in an association with \set-binding and \get-binding.

#5

Seemingly these are implemented in C++, and I guess that it is not possible or easy, otherwise Joris would have implemented smart-ref like that — when converted to LaTeX, they are converted into similar codes in cleveref, which detects the environment instead of the label name, so he should have been well aware of this strategy.

#6

Yes, I’ve tried and I cannot infer the position of a typesetter tree in the document. Another approach, albeit less nice, is to postprocess the document via a scheme script and infer the surrounding environment of a label so that one is able to classify it and then store the information somewhere, so that another typesetting pass over the document can show the correct association between types and labels. This would require at least two passes, but since anyway one has to have a similar mechanism for biblio and ToC, I guess it is not so bad.

#7

We can just create a gui side panel/window to manage and navigate those labels. That would be the most non-destructive way. In addition, those panels/windows can also be used to manage toc and other metadata.

#8

What? I am talking about smart-ref, which determines type of reference. For example, if a label is set at a theorem, then its reference would become “Theorem XXX” (which generates “Theorem”, instead of just a number).

#9

Yes, present implementation has no idea about the context of label. To get the minimal outer context of labels, the first step is to trace those labels within a document. That also allow us to change them simultaneously.