equal
deleted
inserted
replaced
133 (* theory file *) |
133 (* theory file *) |
134 |
134 |
135 val thy_file_setup = |
135 val thy_file_setup = |
136 Thy_Output.antiquotation @{binding thy_file} (Scan.lift Args.name) |
136 Thy_Output.antiquotation @{binding thy_file} (Scan.lift Args.name) |
137 (fn {context = ctxt, ...} => |
137 (fn {context = ctxt, ...} => |
138 fn name => (Thy_Load.check_thy [] Path.current name; Thy_Output.output ctxt [Pretty.str name])); |
138 fn name => (Thy_Load.check_thy Path.current name; Thy_Output.output ctxt [Pretty.str name])); |
139 |
139 |
140 |
140 |
141 (* Isabelle/Isar entities (with index) *) |
141 (* Isabelle/Isar entities (with index) *) |
142 |
142 |
143 local |
143 local |