equal
deleted
inserted
replaced
43 def is_theory: Boolean = node_name.is_theory |
43 def is_theory: Boolean = node_name.is_theory |
44 |
44 |
45 |
45 |
46 /* external file */ |
46 /* external file */ |
47 |
47 |
48 val file: JFile = Url.file(uri).getCanonicalFile |
48 val file: JFile = Url.parse_file(uri).getCanonicalFile |
49 |
49 |
50 def external(b: Boolean): Document_Model = copy(external_file = b) |
50 def external(b: Boolean): Document_Model = copy(external_file = b) |
51 |
51 |
52 def register(watcher: File_Watcher) |
52 def register(watcher: File_Watcher) |
53 { |
53 { |