138 |
138 |
139 local |
139 local |
140 |
140 |
141 val arg = enclose "{" "}" o clean_string; |
141 val arg = enclose "{" "}" o clean_string; |
142 |
142 |
143 fun output_entity markup index kind src ctxt (logic, name) = |
143 fun output_entity markup index kind ctxt (logic, name) = |
144 (case index of |
144 (case index of |
145 NONE => "" |
145 NONE => "" |
146 | SOME is_def => |
146 | SOME is_def => |
147 "\\index" ^ (if is_def then "def" else "ref") ^ arg logic ^ arg kind ^ arg name) |
147 "\\index" ^ (if is_def then "def" else "ref") ^ arg logic ^ arg kind ^ arg name) |
148 ^ |
148 ^ |
149 (Output.output (if ! O.source then str_of_source src else name) |
149 (Output.output name |
150 |> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}") |
150 |> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}") |
151 |> (if ! O.quotes then quote else I) |
151 |> (if ! O.quotes then quote else I) |
152 |> (if ! O.display then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}" |
152 |> (if ! O.display then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}" |
153 else enclose "\\mbox{\\isa{" "}}")); |
153 else enclose "\\mbox{\\isa{" "}}")); |
154 |
154 |
155 fun entity markup index kind = |
155 fun entity markup index kind = |
156 O.args (Scan.lift (Scan.optional (Args.parens Args.name) "" -- Args.name)) |
156 O.args (Scan.lift (Scan.optional (Args.parens Args.name) "" -- Args.name)) |
157 (output_entity markup index kind); |
157 (K (output_entity markup index kind)); |
158 |
158 |
159 fun entity_antiqs markup kind = |
159 fun entity_antiqs markup kind = |
160 [(kind, entity markup NONE kind), |
160 [(kind, entity markup NONE kind), |
161 (kind ^ "_def", entity markup (SOME true) kind), |
161 (kind ^ "_def", entity markup (SOME true) kind), |
162 (kind ^ "_ref", entity markup (SOME false) kind)]; |
162 (kind ^ "_ref", entity markup (SOME false) kind)]; |