13 |
public String span2xml(Span s0) { |
public String span2xml(Span s0) { |
14 |
if(s0 instanceof TextSpan) { |
if(s0 instanceof TextSpan) { |
15 |
TextSpan s = (TextSpan)s0; |
TextSpan s = (TextSpan)s0; |
16 |
return "<" + (namespace == null ? "" : ns+":") + |
return "<" + (namespace == null ? "" : |
17 |
|
namespace+":") + |
18 |
"ts b=\""+s.getScrollBlock().getID()+ |
"ts b=\""+s.getScrollBlock().getID()+ |
19 |
"\" s=\""+s.offset()+ |
"\" s=\""+s.offset()+ |
20 |
"\" e=\""+(s.offset()+s.length())+"\"/>"; |
"\" e=\""+(s.offset()+s.length())+"\"/>"; |
21 |
} else { |
} else { |
22 |
throw new Error("Don't know how to serialize "+s+" yet"); |
throw new Error("Don't know how to serialize "+s0+" yet"); |
23 |
} |
} |
24 |
} |
} |
25 |
|
|